1  /-
  2  Copyright (c) 2018 Scott Morrison. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
  5  -/
  6  import category_theory.whiskering
src         └────────────────────────┘
  7  import category_theory.yoneda
src         └────────────────────┘
  8  import category_theory.limits.cones
src         └──────────────────────────┘
  9  import category_theory.eq_to_hom
src         └───────────────────────┘
 10  
 11  open category_theory category_theory.category category_theory.functor opposite
 12  
 13  namespace category_theory.limits
 14  
 15  universes v u u' u'' w -- declare the `v`'s first; see `category_theory.category` for an explanation
 16  
 17  -- See the notes at the top of cones.lean, explaining why we can't allow `J : Prop` here.
 18  variables {J K : Type v} [small_category J] [small_category K]
id                    └──┘     └────────────┘     └────────────┘
src                            └────────────┘     └────────────┘
typ                   └──┘     └────────────┘     └────────────┘
doc                            └────────────┘     └────────────┘
 19  variables {C : Type u} [𝒞 : category.{v} C]
id                  └──┘         └──────┘
src                              └──────┘
typ                 └──┘         └──────┘
doc                              └──────┘
 20  include 𝒞
 21  
 22  variables {F : J ⥤ C}
id                    
src                   
typ                   
doc                   
 23  
 24  /-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
 25    cone morphism to `t`. -/
 26  structure is_limit (t : cone F) :=
id                           └──┘ 
src                          └──┘
typ                          └──┘ 
doc                          └──┘
 27  (lift  : Π (s : cone F), s.X ⟶ t.X)
id                  └──┘    └┘  └┘
src                 └──┘      └┘   └┘
typ                 └──┘    └┘  └┘
doc                  └──┘
 28  (fac'  : ∀ (s : cone F) (j : J), lift s ≫ t.π.app j = s.π.app j . obviously)
id                  └──┘           └──┘   └┘└──┘   └┘└──┘  
src                 └──┘             └──┘     └┘└──┘     └┘└──┘
typ                 └──┘           └──┘   └┘└──┘   └┘└──┘  
doc                 └──┘
 29  (uniq' : ∀ (s : cone F) (m : s.X ⟶ t.X) (w : ∀ j : J, m ≫ t.π.app j = s.π.app j),
id                  └──┘        └┘  └┘                └┘└──┘   └┘└──┘ 
src                 └──┘          └┘   └┘                    └┘└──┘     └┘└──┘
typ                 └──┘        └┘  └┘                └┘└──┘   └┘└──┘ 
doc                 └──┘
 30    m = lift s . obviously)
id       └──┘  
src       └──┘
typ      └──┘  
 31  
 32  restate_axiom is_limit.fac'
 33  attribute [simp] is_limit.fac
id                    └──────────┘
typ                   └──────────┘
doc             └──┘
 34  restate_axiom is_limit.uniq'
 35  
 36  namespace is_limit
 37  
 38  instance subsingleton {t : cone F} : subsingleton (is_limit t) :=
id                              └──┘     └──────────┘  └──────┘ 
src                             └──┘      └──────────┘  └──────┘
typ                             └──┘     └──────────┘  └──────┘ 
doc                             └──┘                    └──────┘
 39  ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
id                                 
src      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
typ      └────────┘  └────┘  └────┘  └───┘  └─┘  └───────────┘
doc      └────────┘  └────┘   └────┘          └─┘  └───────────┘
txt      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
par      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
pid            └──┘               
st      └──────────────────────────────────────────────────────┘
 40  
 41  /- Repackaging the definition in terms of cone morphisms. -/
 42  
 43  def lift_cone_morphism {t : cone F} (h : is_limit t) (s : cone F) : s ⟶ t :=
id                               └──┘        └──────┘        └──┘       
src                              └──┘         └──────┘         └──┘        
typ                              └──┘        └──────┘        └──┘       
doc                              └──┘         └──────┘         └──┘
 44  { hom := h.lift s }
id           └───┘ 
src           └───┘
typ          └───┘ 
doc  
 45  
 46  lemma uniq_cone_morphism {s t : cone F} (h : is_limit t) {f f' : s ⟶ t} :
id                                   └──┘        └──────┘             
src                                  └──┘         └──────┘              
typ                                  └──┘        └──────┘             
doc                                  └──┘         └──────┘
 47    f = f' :=
id       └┘
src      
typ      └┘
 48  have ∀ {g : s ⟶ t}, g = h.lift_cone_morphism s, by intro g; ext; exact h.uniq _ _ g.w,
id                      └─────────────────┘                          └────┘     └─┘
src                         └─────────────────┘       └─────┘  └─┘  └────┘      └───┘└─┘
typ                     └─────────────────┘      └─────┘  └─┘  └────┘└────┘└───┘└─┘
doc                                                     └─────┘  └─┘  └────┘      └───┘
txt                                                     └─────┘  └─┘  └────┘      └───┘
par                                                     └─────┘  └─┘  └────┘      └───┘
pid                                                          └┘                  └───┘
st                                                     └─────────────────────────────────┘
 49  this.trans this.symm
id   └──┘└────┘ └──┘└───┘
src      └────┘     └───┘
typ  └──┘└────┘ └──┘└───┘
 50  
 51  def mk_cone_morphism {t : cone F}
id                             └──┘ 
src                            └──┘
typ                            └──┘ 
doc                            └──┘
st       └──┘└──────────┘
 52    (lift : Π (s : cone F), s ⟶ t)
id                    └──┘      
src                   └──┘       
typ                   └──┘      
doc                   └──┘
 53    (uniq' : ∀ (s : cone F) (m : s ⟶ t), m = lift s) : is_limit t :=
id                     └──┘               └──┘     └──────┘ 
src                    └──┘                   └──┘      └──────┘
typ                    └──┘               └──┘     └──────┘ 
doc                    └──┘                               └──────┘
 54  { lift := λ s, (lift s).hom,
id                 └──┘  └─┘
src                 └──┘   └─┘
typ                └──┘  └─┘
doc  
 55    uniq' := λ s m w,
id                  
typ                 
 56      have cone_morphism.mk m w = lift s, by apply uniq',
id            └──────────────┘    └──┘ 
src           └──────────────┘      └──┘       └────┘
typ           └──────────────┘    └──┘      └────┘
doc                                             └────┘
txt                                             └────┘
par                                             └────┘
pid                                                  
st                                             └──────────┘
 57      congr_arg cone_morphism.hom this }
id       └───────┘ └───────────────┘ └──┘
src      └───────┘ └───────────────┘
typ      └───────┘ └───────────────┘ └──┘
 58  
 59  /-- Limit cones on `F` are unique up to isomorphism. -/
 60  def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t :=
id                               └──┘        └──────┘        └──────┘       
src                              └──┘         └──────┘         └──────┘        
typ                              └──┘        └──────┘        └──────┘       
doc                              └──┘         └──────┘         └──────┘
 61  { hom := Q.lift_cone_morphism s,
id            └─────────────────┘ 
src            └─────────────────┘
typ           └─────────────────┘ 
 62    inv := P.lift_cone_morphism t,
id            └─────────────────┘ 
src            └─────────────────┘
typ           └─────────────────┘ 
 63    hom_inv_id' := P.uniq_cone_morphism,
id                    └─────────────────┘
src                    └─────────────────┘
typ                   └─────────────────┘
 64    inv_hom_id' := Q.uniq_cone_morphism }
id                    └─────────────────┘
src                    └─────────────────┘
typ                   └─────────────────┘
 65  
 66  def of_iso_limit {r t : cone F} (P : is_limit r) (i : r ≅ t) : is_limit t :=
id                           └──┘        └──────┘              └──────┘ 
src                          └──┘         └──────┘                 └──────┘
typ                          └──┘        └──────┘              └──────┘ 
doc                          └──┘         └──────┘                  └──────┘
 67  is_limit.mk_cone_morphism
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
 68    (λ s, P.lift_cone_morphism s ≫ i.hom)
id          └─────────────────┘   └──┘
src           └─────────────────┘     └──┘
typ         └─────────────────┘   └──┘
 69    (λ s m, by rw ←i.comp_inv_eq; apply P.uniq_cone_morphism)
id         
src               └──┘               └────┘
typ             └──┘└───────────┘  └────┘
doc               └──┘               └────┘
txt               └──┘               └────┘
par               └──┘               └────┘
pid                 └┘                    
st               └────────────────────────────────────────────┘
 70  
 71  variables {t : cone F}
id                  └──┘
src                 └──┘
typ                 └──┘
doc                 └──┘
 72  
 73  lemma hom_lift (h : is_limit t) {W : C} (m : W ⟶ t.X) :
id                       └──────┘                 └┘
src                      └──────┘                     └┘
typ                      └──────┘                 └┘
doc                      └──────┘
 74    m = h.lift { X := W, π := { app := λ b, m ≫ t.π.app b } } :=
id       └───┘                             └┘└──┘ 
src        └───┘                                 └┘└──┘
typ      └───┘                             └┘└──┘ 
doc                              
 75  h.uniq { X := W, π := { app := λ b, m ≫ t.π.app b } } m (λ b, rfl)
id   └───┘                             └┘└──┘            └─┘
src                                         └┘└──┘               └─┘
typ  └───┘                             └┘└──┘            └─┘
doc                        
 76  
 77  /-- Two morphisms into a limit are equal if their compositions with
 78    each cone morphism are equal. -/
 79  lemma hom_ext (h : is_limit t) {W : C} {f f' : W ⟶ t.X}
id                      └──────┘                    └┘
src                     └──────┘                        └┘
typ                     └──────┘                    └┘
doc                     └──────┘
 80    (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) : f = f' :=
id                └┘└──┘   └┘  └┘└──┘       └┘
src                  └┘└──┘         └┘└──┘        
typ               └┘└──┘   └┘  └┘└──┘       └┘
 81  by rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w
id          └────────┘   └────────┘ └┘                └────┘ 
src     └──┘└────────┘ └┘└────────┘    └───┘  └────┘└────┘ 
typ     └──┘└────────┘└┘└────────┘└┘  └───┘  └────┘└────┘
doc     └──┘           └┘                     └────┘       
txt     └──┘           └┘              └───┘  └────┘       
par     └──┘           └┘              └───┘  └────┘       
pid       └┘           └┘                                 
st     └───────────────┘└─────────────┘└───────────────────────
 82  
src  
typ  
doc  
txt  
par  
pid  
st   
 83  /-- The universal property of a limit cone: a map `W ⟶ X` is the same as
 84    a cone on `F` with vertex `W`. -/
 85  def hom_iso (h : is_limit t) (W : C) : (W ⟶ t.X) ≅ ((const J).obj W ⟶ F) :=
id                    └──────┘               └┘     └───┘  └─┘    
src                   └──────┘                   └┘     └───┘   └─┘    
typ                   └──────┘               └┘     └───┘  └─┘    
doc                   └──────┘
 86  { hom := λ f, (t.extend f).π,
id                └─────┘  
src                 └─────┘   
typ               └─────┘  
doc                 └─────┘
 87    inv := λ π, h.lift { X := W, π := π },
id                └───┘               
src                 └───┘
typ               └───┘               
 88    hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
src                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
typ                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
doc                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
txt                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
par                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
pid                         └┘                       └┘                   
st                      └──────────────────────────────────────────────────┘
 89  
 90  @[simp] lemma hom_iso_hom (h : is_limit t) {W : C} (f : W ⟶ t.X) :
id                                  └──────┘                 └┘
src                                 └──────┘                     └┘
typ                                 └──────┘                 └┘
doc    └──┘                         └──────┘
 91    (is_limit.hom_iso h W).hom f = (t.extend f).π := rfl
id      └──────────────┘   └─┘     └─────┘       └─┘
src     └──────────────┘     └─┘       └─────┘        └─┘
typ     └──────────────┘   └─┘     └─────┘       └─┘
doc     └──────────────┘                └─────┘
 92  
 93  /-- The limit of `F` represents the functor taking `W` to
 94    the set of cones on `F` with vertex `W`. -/
 95  def nat_iso (h : is_limit t) : yoneda.obj t.X ≅ F.cones :=
id                    └──────┘     └────┘└──┘ └┘  └────┘
src                   └──────┘      └────┘└──┘  └┘   └────┘
typ                   └──────┘     └────┘└──┘ └┘  └────┘
doc                   └──────┘                        └────┘
 96  nat_iso.of_components (λ W, is_limit.hom_iso h (unop W)) (by tidy).
id   └───────────────────┘      └──────────────┘   └──┘ 
src  └───────────────────┘       └──────────────┘    └──┘         └──┘
typ  └───────────────────┘      └──────────────┘   └──┘        └──┘
doc                              └──────────────┘                 └──┘
txt                                                               └──┘
par                                                               └──┘
st                                                               └───┘
 97  
 98  def hom_iso' (h : is_limit t) (W : C) :
id                     └──────┘        
src                    └──────┘
typ                    └──────┘        
doc                    └──────┘
 99    ((W ⟶ t.X) : Type v) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
id         └┘                        └──┘         └┘         └┘      └──┘    └┘
src          └┘                           └──┘                                  └──┘   
typ        └┘                        └──┘         └┘         └┘      └──┘    └┘
100  h.hom_iso W ≪≫
id   └──────┘  └┘
src   └──────┘   └┘
typ  └──────┘  └┘
doc   └──────┘
101  { hom := λ π,
id             
src  
typ            
doc  
102    ⟨λ j, π.app j, λ j j' f,
id          └──┘      └┘ 
src           └──┘
typ         └──┘      └┘ 
103     by convert ←(π.naturality f).symm; apply id_comp⟩,
id                   └──────────┘               └─────┘
src        └───────┘ └──────────┘ └────┘  └────┘└─────┘
typ        └───────┘ └──────────┘└────┘  └────┘└─────┘
doc        └───────┘              └────┘  └────┘
txt        └───────┘              └────┘  └────┘
par        └───────┘              └────┘  └────┘
pid               └┘              └───┘       
st        └────────────────────────────────────────────┘
104    inv := λ p,
id              
typ             
105    { app := λ j, p.1 j,
id                    
src                   
typ                   
st                  
106      naturality' := λ j j' f, begin dsimp, rw [id_comp], exact (p.2 f).symm end } }
id                         └┘                    └─────┘             
src                                     └───┘  └──┘└─────┘  └────┘  └─┘ └─────┘
typ                        └┘         └───┘  └──┘└─────┘  └────┘ └─┘└─────┘
doc                                     └───┘  └──┘         └────┘  └─┘ └─────┘
txt                                     └───┘  └──┘         └────┘  └─┘ └─────┘
par                                     └───┘  └──┘         └────┘  └─┘ └─────┘
pid                                              └┘                └─┘ └───┘└┘
st                                └─────────┘└───────────┘└────────────────────┘└─┘
107  
108  /-- If G : C → D is a faithful functor which sends t to a limit cone,
109    then it suffices to check that the induced maps for the image of t
110    can be lifted to maps of C. -/
111  def of_faithful {t : cone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [faithful G]
id                        └──┘                  └──────┘                 └──────┘ 
src                       └──┘                   └──────┘                    └──────┘
typ                       └──┘                  └──────┘                 └──────┘ 
doc                       └──┘                   └──────┘                    └──────┘
112    (ht : is_limit (G.map_cone t)) (lift : Π (s : cone F), s.X ⟶ t.X)
id           └──────┘  └───────┘                   └──┘    └┘  └┘
src          └──────┘   └───────┘                    └──┘      └┘   └┘
typ          └──────┘  └───────┘                   └──┘    └┘  └┘
doc          └──────┘   └───────┘                    └──┘
113    (h : ∀ s, G.map (lift s) = ht.lift (G.map_cone s)) : is_limit t :=
id              └──┘  └──┘    └┘└───┘  └───────┘      └──────┘ 
src               └──┘  └──┘       └───┘   └───────┘       └──────┘
typ             └──┘  └──┘    └┘└───┘  └───────┘      └──────┘ 
doc                                         └───────┘       └──────┘
114  { lift := lift,
id             └──┘
src            └──┘
typ            └──┘
115    fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
id                                                          
src                      └────┘               └──┘          └┘   └────┘
typ                    └────┘               └──┘└────────┘└┘  └────┘
doc                      └────┘               └──┘          └┘   └────┘
txt                      └────┘               └──┘          └┘   └────┘
par                      └────┘               └──┘          └┘   └────┘
pid                                            └┘          └┘        
st                      └────────────────────────┘└────────┘└─┘└────────────┘
116    uniq' := λ s m w, begin
id                  
typ                 
st                       └─────
117      apply G.injectivity, rw h,
id                               
src      └────┘               └─┘
typ      └────┘               └─┘
doc      └────┘               └─┘
txt      └────┘               └─┘
par      └────┘               └─┘
pid                            
st   ──────────────────────┘└────┘└─
118      refine ht.uniq (G.map_cone s) _ (λ j, _),
id              └─────┘  └────────┘ 
src      └─────┘        └────────┘ └──┘  └────┘
typ      └─────┘└─────┘ └────────┘└──┘  └────┘
doc      └─────┘        └────────┘ └──┘  └────┘
txt      └─────┘                   └──┘  └────┘
par      └─────┘                   └──┘  └────┘
pid                               └──┘  └────┘
st   ───────────────────────────────────────────┘└─
119      convert ←congr_arg (λ f, G.map f) (w j),
id                └───────┘       └───┘      
src      └───────┘└───────┘  └──┘└───┘ └┘   
typ      └───────┘└───────┘  └──┘└───┘ └┘ 
doc      └───────┘           └──┘      └┘   
txt      └───────┘           └──┘      └┘   
par      └───────┘           └──┘      └┘   
pid             └┘           └──┘      └┘   
st   ──────────────────────────────────────────┘└─
120      apply G.map_comp
src      └────┘          
typ      └────┘          
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ─────────────────────
121    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
122  
123  def iso_unique_cone_morphism {t : cone F} :
id                                     └──┘ 
src                                    └──┘
typ                                    └──┘ 
doc                                    └──┘
124    is_limit t ≅ Π s, unique (s ⟶ t) :=
id     └──────┘       └────┘    
src    └──────┘         └────┘    
typ    └──────┘       └────┘    
doc    └──────┘
125  { hom := λ h s,
id              
src  
typ             
doc  
126    { default := h.lift_cone_morphism s,
id                  └─────────────────┘ 
src                  └─────────────────┘
typ                 └─────────────────┘ 
127      uniq := λ _, h.uniq_cone_morphism },
id                   └─────────────────┘
src                    └─────────────────┘
typ                  └─────────────────┘
128    inv := λ h,
id              
typ             
129    { lift := λ s, (h s).default.hom,
id                     └─────┘ └─┘
src                       └─────┘ └─┘
typ                    └─────┘ └─┘
doc    
130      uniq' := λ s f w, congr_arg cone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
id                      └───────┘ └───────────────┘     └──┘     
src                        └───────┘ └───────────────┘       └──┘
typ                     └───────┘ └───────────────┘     └──┘     
131  
132  namespace of_nat_iso
133  variables {X : C} (h : yoneda.obj X ≅ F.cones)
id                          └────┘└──┘     └────┘
src                         └────┘└──┘     └────┘
typ                         └────┘└──┘     └────┘
doc                                         └────┘
134  
135  /-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point `Y`. -/
136  def cone_of_hom {Y : C} (f : Y ⟶ X) : cone F :=
id                                     └──┘ 
src                                       └──┘
typ                                    └──┘ 
doc                                        └──┘
137  { X := Y, π := h.hom.app (op Y) f }
id                 └──┘└──┘  └┘   
src                  └──┘└──┘  └┘
typ                └──┘└──┘  └┘   
138  
139  /-- If `F.cones` is represented by `X`, each cone `s` gives a morphism `s.X ⟶ X`. -/
140  def hom_of_cone (s : cone F) : s.X ⟶ X := h.inv.app (op s.X) s.π
id                        └──┘     └┘      └──┘└──┘  └┘ └┘  └┘
src                       └──┘       └┘        └──┘└──┘  └┘  └┘   └┘
typ                       └──┘     └┘      └──┘└──┘  └┘ └┘  └┘
doc                       └──┘
141  
142  @[simp] lemma cone_of_hom_of_cone (s : cone F) : cone_of_hom h (hom_of_cone h s) = s :=
id                                          └──┘     └─────────┘   └─────────┘     
src                                         └──┘      └─────────┘    └─────────┘      
typ                                         └──┘     └─────────┘   └─────────┘     
doc    └──┘                                 └──┘      └─────────┘    └─────────┘
143  begin
st   └─────
144    dsimp [cone_of_hom, hom_of_cone], cases s, congr, dsimp,
id            └─────────┘  └─────────┘         
src    └─────┘└─────────┘└┘└─────────┘  └────┘   └───┘  └───┘
typ    └─────┘└─────────┘└┘└─────────┘  └────┘  └───┘  └───┘
doc    └─────┘└─────────┘└┘└─────────┘  └────┘          └───┘
txt    └─────┘           └┘             └────┘   └───┘  └───┘
par    └─────┘           └┘             └────┘   └───┘  └───┘
pid                    └┘                  
st   ─────────────────────────────────┘└───────┘└─────┘└─────┘└─
145    exact congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) (op s_X)) s_π,
id                      └───────┘  └───────┘ └───────────┘ └──────────┘   └┘ └─┘   └─┘
src    └────┘          └───────┘ └───────┘└───────────┘└──────────┘└┘ └┘   └─┘
typ    └────┘          └───────┘ └───────┘└───────────┘└──────────┘└┘ └┘└─┘└─┘└─┘
doc    └────┘                                                      └┘      └─┘
txt    └────┘                                                      └┘      └─┘
par    └────┘                                                      └┘      └─┘
pid                                                               └┘      └─┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
146  end
st   ──┘
147  
148  @[simp] lemma hom_of_cone_of_hom {Y : C} (f : Y ⟶ X) : hom_of_cone h (cone_of_hom h f) = f :=
id                                                      └─────────┘   └─────────┘     
src                                                        └─────────┘    └─────────┘      
typ                                                     └─────────┘   └─────────┘     
doc    └──┘                                                 └─────────┘    └─────────┘
149  congr_fun (congr_fun (congr_arg nat_trans.app h.hom_inv_id) (op Y)) f
id   └───────┘  └───────┘  └───────┘ └───────────┘ └─────────┘   └┘    
src  └───────┘  └───────┘  └───────┘ └───────────┘  └─────────┘   └┘
typ  └───────┘  └───────┘  └───────┘ └───────────┘ └─────────┘   └┘    
150  
151  /-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X`
152  will be a limit cone. -/
153  def limit_cone : cone F :=
id                    └──┘ 
src                   └──┘
typ                   └──┘ 
doc                   └──┘
154  cone_of_hom h (𝟙 X)
id   └─────────┘    
src  └─────────┘    
typ  └─────────┘    
doc  └─────────┘
155  
156  /-- If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is
157  the limit cone extended by `f`. -/
158  lemma cone_of_hom_fac {Y : C} (f : Y ⟶ X) :
id                                       
src                                       
typ                                      
159  cone_of_hom h f = (limit_cone h).extend f :=
id   └─────────┘     └────────┘  └────┘  
src  └─────────┘       └────────┘   └────┘
typ  └─────────┘     └────────┘  └────┘  
doc  └─────────┘        └────────┘   └────┘
160  begin
st   └─────
161    dsimp [cone_of_hom, limit_cone, cone.extend],
id            └─────────┘  └────────┘  └─────────┘
src    └─────┘└─────────┘└┘└────────┘└┘└─────────┘
typ    └─────┘└─────────┘└┘└────────┘└┘└─────────┘
doc    └─────┘└─────────┘└┘└────────┘└┘└─────────┘
txt    └─────┘           └┘          └┘           
par    └─────┘           └┘          └┘           
pid                    └┘          └┘           
st   ─────────────────────────────────────────────┘└─
162    congr,
src    └───┘
typ    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
163    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
164    have t := congr_fun (h.hom.naturality f.op) (𝟙 X),
id               └───────┘  └──────────────┘ └──┘    
src    └────────┘└───────┘ └──────────────┘└──┘└┘  
typ    └────────┘└───────┘ └──────────────┘└──┘└┘ 
doc    └────────┘                              └┘   
txt    └────────┘                              └┘   
par    └────────┘                              └┘   
pid    └────┘└─┘                              └┘   
st   ──────────────────────────────────────────────────┘└─
165    dsimp at t,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid         └──┘
st   ───────────┘└─
166    simp only [comp_id] at t,
id                └─────┘
src    └─────────┘└─────┘└────┘
typ    └─────────┘└─────┘└────┘
doc    └─────────┘       └────┘
txt    └─────────┘       └────┘
par    └─────────┘       └────┘
pid        └──┘└┘       └──┘
st   ─────────────────────────┘└─
167    rw congr_fun (congr_arg nat_trans.app t) j,
id        └───────┘  └───────┘ └───────────┘   
src    └─┘└───────┘ └───────┘└───────────┘ └┘
typ    └─┘└───────┘ └───────┘└───────────┘└┘
doc    └─┘                                 └┘
txt    └─┘                                 └┘
par    └─┘                                 └┘
pid                                       └┘
st   ───────────────────────────────────────────┘└─
168    refl,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
169  end
st   ──┘
170  
171  /-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
172  corresponding morphism. -/
173  lemma cone_fac (s : cone F) : (limit_cone h).extend (hom_of_cone h s) = s :=
id                       └──┘      └────────┘  └────┘   └─────────┘     
src                      └──┘       └────────┘   └────┘   └─────────┘      
typ                      └──┘      └────────┘  └────┘   └─────────┘     
doc                      └──┘       └────────┘   └────┘   └─────────┘
174  begin
st   └─────
175    rw ←cone_of_hom_of_cone h s,
id         └─────────────────┘  
src    └──┘└─────────────────┘ 
typ    └──┘└─────────────────┘
doc    └──┘                    
txt    └──┘                    
par    └──┘                    
pid      └┘                    
st   ────────────────────────────┘└─
176    conv_lhs { simp only [hom_of_cone_of_hom] },
id                           └────────────────┘
src    └─────────┘└─────────┘└────────────────┘└┘
typ    └─────────┘└─────────┘└────────────────┘└┘
txt    └─────────┘└─────────┘                  └┘
par    └─────────┘└─────────┘                  └┘
pid            └───────────┘                  └─┘
st   ───────────┘└──────────────────────────────┘└┘
177    apply (cone_of_hom_fac _ _).symm,
id            └─────────────┘
src    └────┘ └─────────────┘└────────┘
typ    └────┘ └─────────────┘└────────┘
doc    └────┘ └─────────────┘└────────┘
txt    └────┘                └────────┘
par    └────┘                └────────┘
pid                         └───────┘
st   ─────────────────────────────────┘└─
178  end
st   ──┘
179  
180  end of_nat_iso
181  
182  section
183  open of_nat_iso
184  
185  /--
186  If `F.cones` is representable, then the cone corresponding to the identity morphism on
187  the representing object is a limit cone.
188  -/
189  def of_nat_iso {X : C} (h : yoneda.obj X ≅ F.cones) :
id                              └────┘└──┘   └────┘
src                              └────┘└──┘     └────┘
typ                             └────┘└──┘   └────┘
doc                                              └────┘
190    is_limit (limit_cone h) :=
id     └──────┘  └────────┘ 
src    └──────┘  └────────┘
typ    └──────┘  └────────┘ 
doc    └──────┘  └────────┘
191  { lift := λ s, hom_of_cone h s,
id                 └─────────┘  
src                 └─────────┘
typ                └─────────┘  
doc                 └─────────┘
192    fac' := λ s j,
id                
typ               
193    begin
st     └─────
194      have h := cone_fac h s,
id                 └──────┘  
src      └────────┘└──────┘ 
typ      └────────┘└──────┘
doc      └────────┘└──────┘ 
txt      └────────┘         
par      └────────┘         
pid      └────┘└─┘         
st   ─────────────────────────┘└─
195      cases s,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
196      injection h with h₁ h₂,
id                 
src      └────────┘ └─────────┘
typ      └────────┘└─────────┘
doc      └────────┘ └─────────┘
txt      └────────┘ └─────────┘
par      └────────┘ └─────────┘
pid                └─────────┘
st   ─────────────────────────┘└─
197      simp only [heq_iff_eq] at h₂,
id                  └────────┘
src      └─────────┘└────────┘└─────┘
typ      └─────────┘└────────┘└─────┘
doc      └─────────┘          └─────┘
txt      └─────────┘          └─────┘
par      └─────────┘          └─────┘
pid          └──┘└┘          └───┘
st   ───────────────────────────────┘└─
198      conv_rhs { rw ← h₂ }, refl,
id                       └┘
src      └─────────┘└───┘    └──┘
typ      └─────────┘└───┘└┘  └──┘
doc                            └──┘
txt      └─────────┘└───┘    └──┘
par      └─────────┘└───┘    └──┘
pid              └─────┘  └┘
st   ─────────────┘└───────┘└┘└───┘└─
199    end,
st   ────┘
200    uniq' := λ s m w,
id                  
typ                 
201    begin
st     └─────
202      rw ←hom_of_cone_of_hom h m,
id           └────────────────┘  
src      └──┘└────────────────┘ 
typ      └──┘└────────────────┘
doc      └──┘                   
txt      └──┘                   
par      └──┘                   
pid        └┘                   
st   ─────────────────────────────┘└─
203      congr,
src      └───┘
typ      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
204      rw cone_of_hom_fac,
id          └─────────────┘
src      └─┘└─────────────┘
typ      └─┘└─────────────┘
doc      └─┘└─────────────┘
txt      └─┘
par      └─┘
pid        
st   ─────────────────────┘└─
205      dsimp, cases s, congr,
id                    
src      └───┘  └────┘   └───┘
typ      └───┘  └────┘  └───┘
doc      └───┘  └────┘
txt      └───┘  └────┘   └───┘
par      └───┘  └────┘   └───┘
pid                  
st   ────────┘└───────┘└─────┘└─
206      ext j, exact w j,
id                     
src      └───┘  └────┘ 
typ      └───┘  └────┘
doc      └───┘  └────┘ 
txt      └───┘  └────┘ 
par      └───┘  └────┘ 
pid         └┘        
st   ────────┘└─────────┘└─
207    end }
st   ────┘
208  end
209  
210  end is_limit
211  
212  /-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
213    cocone morphism from `t`. -/
214  structure is_colimit (t : cocone F) :=
id                             └────┘ 
src                            └────┘
typ                            └────┘ 
doc                            └────┘
215  (desc  : Π (s : cocone F), t.X ⟶ s.X)
id                  └────┘    └┘  └┘
src                  └────┘      └┘   └┘
typ                 └────┘    └┘  └┘
doc                  └────┘
216  (fac'  : ∀ (s : cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j . obviously)
id                  └────┘           └┘└──┘   └──┘   └┘└──┘  
src                 └────┘              └┘└──┘             └┘└──┘
typ                 └────┘           └┘└──┘   └──┘   └┘└──┘  
doc                 └────┘
217  (uniq' : ∀ (s : cocone F) (m : t.X ⟶ s.X) (w : ∀ j : J, t.ι.app j ≫ m = s.ι.app j),
id                  └────┘        └┘  └┘              └┘└──┘     └┘└──┘ 
src                 └────┘          └┘   └┘                 └┘└──┘        └┘└──┘
typ                 └────┘        └┘  └┘              └┘└──┘     └┘└──┘ 
doc                 └────┘
218    m = desc s . obviously)
id       └──┘  
src      
typ      └──┘  
219  
220  restate_axiom is_colimit.fac'
221  attribute [simp] is_colimit.fac
id                    └────────────┘
typ                   └────────────┘
doc             └──┘
222  restate_axiom is_colimit.uniq'
223  
224  namespace is_colimit
225  
226  instance subsingleton {t : cocone F} : subsingleton (is_colimit t) :=
id                              └────┘     └──────────┘  └────────┘ 
src                             └────┘      └──────────┘  └────────┘
typ                             └────┘     └──────────┘  └────────┘ 
doc                             └────┘                    └────────┘
227  ⟨by intros P Q; cases P; cases Q; congr; ext; solve_by_elim⟩
id                                 
src      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
typ      └────────┘  └────┘  └────┘  └───┘  └─┘  └───────────┘
doc      └────────┘  └────┘   └────┘          └─┘  └───────────┘
txt      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
par      └────────┘  └────┘   └────┘   └───┘  └─┘  └───────────┘
pid            └──┘               
st      └──────────────────────────────────────────────────────┘
228  
229  /- Repackaging the definition in terms of cone morphisms. -/
230  
231  def desc_cocone_morphism {t : cocone F} (h : is_colimit t) (s : cocone F) : t ⟶ s :=
id                                 └────┘        └────────┘        └────┘       
src                                └────┘         └────────┘         └────┘        
typ                                └────┘        └────────┘        └────┘       
doc                                └────┘         └────────┘         └────┘
232  { hom := h.desc s }
id           └───┘ 
src           └───┘
typ          └───┘ 
doc  
233  
234  lemma uniq_cocone_morphism {s t : cocone F} (h : is_colimit t) {f f' : t ⟶ s} :
id                                     └────┘        └────────┘             
src                                    └────┘         └────────┘              
typ                                    └────┘        └────────┘             
doc                                    └────┘         └────────┘
235    f = f' :=
id       └┘
src      
typ      └┘
236  have ∀ {g : t ⟶ s}, g = h.desc_cocone_morphism s, by intro g; ext; exact h.uniq _ _ g.w,
id                      └───────────────────┘                          └────┘     └─┘
src                         └───────────────────┘       └─────┘  └─┘  └────┘      └───┘└─┘
typ                     └───────────────────┘      └─────┘  └─┘  └────┘└────┘└───┘└─┘
doc                                                       └─────┘  └─┘  └────┘      └───┘
txt                                                       └─────┘  └─┘  └────┘      └───┘
par                                                       └─────┘  └─┘  └────┘      └───┘
pid                                                            └┘                  └───┘
st                                                       └─────────────────────────────────┘
237  this.trans this.symm
id   └──┘└────┘ └──┘└───┘
src      └────┘     └───┘
typ  └──┘└────┘ └──┘└───┘
238  
239  def mk_cocone_morphism {t : cocone F}
id                               └────┘ 
src                              └────┘
typ                              └────┘ 
doc                              └────┘
240    (desc : Π (s : cocone F), t ⟶ s)
id                    └────┘      
src                   └────┘       
typ                   └────┘      
doc                   └────┘
241    (uniq' : ∀ (s : cocone F) (m : t ⟶ s), m = desc s) : is_colimit t :=
id                     └────┘               └──┘     └────────┘ 
src                    └────┘                             └────────┘
typ                    └────┘               └──┘     └────────┘ 
doc                    └────┘                               └────────┘
242  { desc := λ s, (desc s).hom,
id                 └──┘  └─┘
src                        └─┘
typ                └──┘  └─┘
doc  
243    uniq' := λ s m w,
id                  
typ                 
244      have cocone_morphism.mk m w = desc s, by apply uniq',
id            └────────────────┘    └──┘ 
src           └────────────────┘                 └────┘
typ           └────────────────┘    └──┘      └────┘
doc                                               └────┘
txt                                               └────┘
par                                               └────┘
pid                                                    
st                                               └──────────┘
245      congr_arg cocone_morphism.hom this }
id       └───────┘ └─────────────────┘ └──┘
src      └───────┘ └─────────────────┘
typ      └───────┘ └─────────────────┘ └──┘
246  
247  /-- Limit cones on `F` are unique up to isomorphism. -/
248  def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s ≅ t :=
id                               └────┘        └────────┘        └────────┘       
src                              └────┘         └────────┘         └────────┘        
typ                              └────┘        └────────┘        └────────┘       
doc                              └────┘         └────────┘         └────────┘
249  { hom := P.desc_cocone_morphism t,
id            └───────────────────┘ 
src            └───────────────────┘
typ           └───────────────────┘ 
250    inv := Q.desc_cocone_morphism s,
id            └───────────────────┘ 
src            └───────────────────┘
typ           └───────────────────┘ 
251    hom_inv_id' := P.uniq_cocone_morphism,
id                    └───────────────────┘
src                    └───────────────────┘
typ                   └───────────────────┘
252    inv_hom_id' := Q.uniq_cocone_morphism }
id                    └───────────────────┘
src                    └───────────────────┘
typ                   └───────────────────┘
253  
254  def of_iso_colimit {r t : cocone F} (P : is_colimit r) (i : r ≅ t) : is_colimit t :=
id                             └────┘        └────────┘              └────────┘ 
src                            └────┘         └────────┘                 └────────┘
typ                            └────┘        └────────┘              └────────┘ 
doc                            └────┘         └────────┘                  └────────┘
255  is_colimit.mk_cocone_morphism
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
256    (λ s, i.inv ≫ P.desc_cocone_morphism s)
id          └──┘  └───────────────────┘ 
src           └──┘   └───────────────────┘
typ         └──┘  └───────────────────┘ 
257    (λ s m, by rw i.eq_inv_comp; apply P.uniq_cocone_morphism)
id         
src               └─┘               └────┘
typ             └─┘└───────────┘  └────┘
doc               └─┘               └────┘
txt               └─┘               └────┘
par               └─┘               └────┘
pid                                     
st               └─────────────────────────────────────────────┘
258  
259  variables {t : cocone F}
id                  └────┘
src                 └────┘
typ                 └────┘
doc                 └────┘
260  
261  lemma hom_desc (h : is_colimit t) {W : C} (m : t.X ⟶ W) :
id                       └────────┘               └┘  
src                      └────────┘                  └┘ 
typ                      └────────┘               └┘  
doc                      └────────┘
262    m = h.desc { X := W, ι := { app := λ b, t.ι.app b ≫ m,
id       └───┘                            └┘└──┘   
src        └───┘                               └┘└──┘   
typ      └───┘                            └┘└──┘   
263      naturality' := by intros; erw [←assoc, t.ι.naturality, comp_id, comp_id] } } :=
id                                       └───┘                  └─────┘  └─────┘
src                        └────┘  └────┘└───┘└┘              └┘└─────┘└┘└─────┘└┘
typ                        └────┘  └────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────┘└┘
doc                        └────┘  └────┘     └┘              └┘       └┘       └┘
txt                        └────┘  └────┘     └┘              └┘       └┘       └┘
par                        └────┘  └────┘     └┘              └┘       └┘       └┘
pid                                   └─┘     └┘              └┘       └┘       
st                        └────────────┘└────┘└──────────────┘└───────┘└───────┘
264  h.uniq { X := W, ι := { app := λ b, t.ι.app b ≫ m, naturality' := _ } } m (λ b, rfl)
id   └───┘                            └┘└──┘                                └─┘
src                                       └┘└──┘                                    └─┘
typ  └───┘                            └┘└──┘                                └─┘
265  
266  /-- Two morphisms out of a colimit are equal if their compositions with
267    each cocone morphism are equal. -/
268  lemma hom_ext (h : is_colimit t) {W : C} {f f' : t.X ⟶ W}
id                      └────────┘                  └┘  
src                     └────────┘                     └┘ 
typ                     └────────┘                  └┘  
doc                     └────────┘
269    (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f' :=
id              └┘└──┘     └┘└──┘   └┘      └┘
src               └┘└──┘        └┘└──┘            
typ             └┘└──┘     └┘└──┘   └┘      └┘
270  by rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w
id          └────────┘   └────────┘ └┘                └────┘ 
src     └──┘└────────┘ └┘└────────┘    └───┘  └────┘└────┘ 
typ     └──┘└────────┘└┘└────────┘└┘  └───┘  └────┘└────┘
doc     └──┘           └┘                     └────┘       
txt     └──┘           └┘              └───┘  └────┘       
par     └──┘           └┘              └───┘  └────┘       
pid       └┘           └┘                                 
st     └───────────────┘└─────────────┘└───────────────────────
271  
src  
typ  
doc  
txt  
par  
pid  
st   
272  /-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
273    a cocone on `F` with vertex `W`. -/
274  def hom_iso (h : is_colimit t) (W : C) : (t.X ⟶ W) ≅ (F ⟶ (const J).obj W) :=
id                    └────────┘             └┘         └───┘  └─┘  
src                   └────────┘                └┘           └───┘   └─┘
typ                   └────────┘             └┘         └───┘  └─┘  
doc                   └────────┘
275  { hom := λ f, (t.extend f).ι,
id                └─────┘  
src                 └─────┘   
typ               └─────┘  
doc                 └─────┘
276    inv := λ ι, h.desc { X := W, ι := ι },
id                └───┘               
src                 └───┘
typ               └───┘               
277    hom_inv_id' := by ext f; apply h.hom_ext; intro j; simp; dsimp; refl }
src                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
typ                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
doc                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
txt                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
par                      └───┘  └────┘           └─────┘  └──┘  └───┘  └───┘
pid                         └┘                       └┘                   
st                      └──────────────────────────────────────────────────┘
278  
279  @[simp] lemma hom_iso_hom (h : is_colimit t) {W : C} (f : t.X ⟶ W) :
id                                  └────────┘               └┘  
src                                 └────────┘                  └┘ 
typ                                 └────────┘               └┘  
doc    └──┘                         └────────┘
280    (is_colimit.hom_iso h W).hom f = (t.extend f).ι := rfl
id      └────────────────┘   └─┘     └─────┘       └─┘
src     └────────────────┘     └─┘       └─────┘        └─┘
typ     └────────────────┘   └─┘     └─────┘       └─┘
doc     └────────────────┘                └─────┘
281  
282  /-- The colimit of `F` represents the functor taking `W` to
283    the set of cocones on `F` with vertex `W`. -/
284  def nat_iso (h : is_colimit t) : coyoneda.obj (op t.X) ≅ F.cocones :=
id                    └────────┘     └──────┘└──┘  └┘ └┘   └──────┘
src                   └────────┘      └──────┘└──┘  └┘  └┘    └──────┘
typ                   └────────┘     └──────┘└──┘  └┘ └┘   └──────┘
doc                   └────────┘                               └──────┘
285  nat_iso.of_components (is_colimit.hom_iso h) (by intros; ext; dsimp; rw ←assoc; refl)
id   └───────────────────┘  └────────────────┘                               └───┘
src  └───────────────────┘  └────────────────┘        └────┘  └─┘  └───┘  └──┘└───┘  └──┘
typ  └───────────────────┘  └────────────────┘       └────┘  └─┘  └───┘  └──┘└───┘  └──┘
doc                         └────────────────┘        └────┘  └─┘  └───┘  └──┘       └──┘
txt                                                   └────┘  └─┘  └───┘  └──┘       └──┘
par                                                   └────┘  └─┘  └───┘  └──┘       └──┘
pid                                                                         └┘
st                                                   └──────────────────────────────────┘
286  
287  def hom_iso' (h : is_colimit t) (W : C) :
id                     └────────┘        
src                    └────────┘
typ                    └────────┘        
doc                    └────────┘
288    ((t.X ⟶ W) : Type v) ≅ { p : Π j, F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
id       └┘                        └──┘                          └┘   └──┘    └┘   
src       └┘                           └──┘                                    └──┘         
typ      └┘                        └──┘                          └┘   └──┘    └┘   
289  h.hom_iso W ≪≫
id   └──────┘  └┘
src   └──────┘   └┘
typ  └──────┘  └┘
doc   └──────┘
290  { hom := λ ι,
id             
src  
typ            
doc  
291    ⟨λ j, ι.app j, λ j j' f,
id          └──┘      └┘ 
src           └──┘
typ         └──┘      └┘ 
292     by convert ←(ι.naturality f); apply comp_id⟩,
id                   └──────────┘          └─────┘
src        └───────┘ └──────────┘   └────┘└─────┘
typ        └───────┘ └──────────┘  └────┘└─────┘
doc        └───────┘                └────┘
txt        └───────┘                └────┘
par        └───────┘                └────┘
pid               └┘                     
st        └───────────────────────────────────────┘
293    inv := λ p,
id              
typ             
294    { app := λ j, p.1 j,
id                    
src                   
typ                   
295      naturality' := λ j j' f, begin dsimp, rw [comp_id], exact (p.2 f) end } }
id                         └┘                    └─────┘             
src                                     └───┘  └──┘└─────┘  └────┘  └─┘ └┘
typ                        └┘         └───┘  └──┘└─────┘  └────┘ └─┘└┘
doc                                     └───┘  └──┘         └────┘  └─┘ └┘
txt                                     └───┘  └──┘         └────┘  └─┘ └┘
par                                     └───┘  └──┘         └────┘  └─┘ └┘
pid                                              └┘                └─┘ 
st                                └─────────┘└───────────┘└───────────────┘└─┘
296  
297  /-- If G : C → D is a faithful functor which sends t to a colimit cocone,
298    then it suffices to check that the induced maps for the image of t
299    can be lifted to maps of C. -/
300  def of_faithful {t : cocone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [faithful G]
id                        └────┘                  └──────┘                 └──────┘ 
src                       └────┘                   └──────┘                    └──────┘
typ                       └────┘                  └──────┘                 └──────┘ 
doc                       └────┘                   └──────┘                    └──────┘
301    (ht : is_colimit (G.map_cocone t)) (desc : Π (s : cocone F), t.X ⟶ s.X)
id           └────────┘  └─────────┘                   └────┘    └┘  └┘
src          └────────┘   └─────────┘                    └────┘      └┘   └┘
typ          └────────┘  └─────────┘                   └────┘    └┘  └┘
doc          └────────┘   └─────────┘                    └────┘
302    (h : ∀ s, G.map (desc s) = ht.desc (G.map_cocone s)) : is_colimit t :=
id              └──┘  └──┘    └┘└───┘  └─────────┘      └────────┘ 
src               └──┘             └───┘   └─────────┘       └────────┘
typ             └──┘  └──┘    └┘└───┘  └─────────┘      └────────┘ 
doc                                         └─────────┘       └────────┘
303  { desc := desc,
id             └──┘
typ            └──┘
304    fac' := λ s j, by apply G.injectivity; rw [G.map_comp, h]; apply ht.fac,
id                                                          
src                      └────┘               └──┘          └┘   └────┘
typ                    └────┘               └──┘└────────┘└┘  └────┘
doc                      └────┘               └──┘          └┘   └────┘
txt                      └────┘               └──┘          └┘   └────┘
par                      └────┘               └──┘          └┘   └────┘
pid                                            └┘          └┘        
st                      └────────────────────────┘└────────┘└─┘└────────────┘
305    uniq' := λ s m w, begin
id                  
typ                 
st                       └─────
306      apply G.injectivity, rw h,
id                               
src      └────┘               └─┘
typ      └────┘               └─┘
doc      └────┘               └─┘
txt      └────┘               └─┘
par      └────┘               └─┘
pid                            
st   ──────────────────────┘└────┘└─
307      refine ht.uniq (G.map_cocone s) _ (λ j, _),
id              └─────┘  └──────────┘ 
src      └─────┘        └──────────┘ └──┘  └────┘
typ      └─────┘└─────┘ └──────────┘└──┘  └────┘
doc      └─────┘        └──────────┘ └──┘  └────┘
txt      └─────┘                     └──┘  └────┘
par      └─────┘                     └──┘  └────┘
pid                                 └──┘  └────┘
st   ─────────────────────────────────────────────┘└─
308      convert ←congr_arg (λ f, G.map f) (w j),
id                └───────┘       └───┘      
src      └───────┘└───────┘  └──┘└───┘ └┘   
typ      └───────┘└───────┘  └──┘└───┘ └┘ 
doc      └───────┘           └──┘      └┘   
txt      └───────┘           └──┘      └┘   
par      └───────┘           └──┘      └┘   
pid             └┘           └──┘      └┘   
st   ──────────────────────────────────────────┘└─
309      apply G.map_comp
src      └────┘          
typ      └────┘          
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ─────────────────────
310    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
311  
312  def iso_unique_cocone_morphism {t : cocone F} :
id                                       └────┘ 
src                                      └────┘
typ                                      └────┘ 
doc                                      └────┘
313    is_colimit t ≅ Π s, unique (t ⟶ s) :=
id     └────────┘       └────┘    
src    └────────┘         └────┘    
typ    └────────┘       └────┘    
doc    └────────┘
314  { hom := λ h s,
id              
src  
typ             
doc  
315    { default := h.desc_cocone_morphism s,
id                  └───────────────────┘ 
src                  └───────────────────┘
typ                 └───────────────────┘ 
316      uniq := λ _, h.uniq_cocone_morphism },
id                   └───────────────────┘
src                    └───────────────────┘
typ                  └───────────────────┘
317    inv := λ h,
id              
typ             
318    { desc := λ s, (h s).default.hom,
id                     └─────┘ └─┘
src                       └─────┘ └─┘
typ                    └─────┘ └─┘
doc    
319      uniq' := λ s f w, congr_arg cocone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
id                      └───────┘ └─────────────────┘     └──┘     
src                        └───────┘ └─────────────────┘       └──┘
typ                     └───────┘ └─────────────────┘     └──┘     
320  
321  namespace of_nat_iso
322  variables {X : C} (h : coyoneda.obj (op X) ≅ F.cocones)
id                          └──────┘└──┘  └┘      └──────┘
src                         └──────┘└──┘  └┘      └──────┘
typ                         └──────┘└──┘  └┘      └──────┘
doc                                                └──────┘
323  
324  /-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone point `Y`. -/
325  def cocone_of_hom {Y : C} (f : X ⟶ Y) : cocone F :=
id                                       └────┘ 
src                                         └────┘
typ                                      └────┘ 
doc                                          └────┘
326  { X := Y, ι := h.hom.app Y f }
id                 └──┘└──┘  
src                  └──┘└──┘
typ                └──┘└──┘  
327  
328  /-- If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.X`. -/
329  def hom_of_cocone (s : cocone F) : X ⟶ s.X := h.inv.app s.X s.ι
id                          └────┘       └┘    └──┘└──┘ └┘ └┘
src                         └────┘          └┘     └──┘└──┘  └┘  └┘
typ                         └────┘       └┘    └──┘└──┘ └┘ └┘
doc                         └────┘
330  
331  @[simp] lemma cocone_of_hom_of_cocone (s : cocone F) : cocone_of_hom h (hom_of_cocone h s) = s :=
id                                              └────┘     └───────────┘   └───────────┘     
src                                             └────┘      └───────────┘    └───────────┘      
typ                                             └────┘     └───────────┘   └───────────┘     
doc    └──┘                                     └────┘      └───────────┘    └───────────┘
332  begin
st   └─────
333    dsimp [cocone_of_hom, hom_of_cocone], cases s, congr, dsimp,
id            └───────────┘  └───────────┘         
src    └─────┘└───────────┘└┘└───────────┘  └────┘   └───┘  └───┘
typ    └─────┘└───────────┘└┘└───────────┘  └────┘  └───┘  └───┘
doc    └─────┘└───────────┘└┘└───────────┘  └────┘          └───┘
txt    └─────┘             └┘               └────┘   └───┘  └───┘
par    └─────┘             └┘               └────┘   └───┘  └───┘
pid                      └┘                    
st   ─────────────────────────────────────┘└───────┘└─────┘└─────┘└─
334    exact congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) s_X) s_ι,
id                      └───────┘  └───────┘ └───────────┘ └──────────┘  └─┘  └─┘
src    └────┘          └───────┘ └───────┘└───────────┘└──────────┘└┘   └┘
typ    └────┘          └───────┘ └───────┘└───────────┘└──────────┘└┘└─┘└┘└─┘
doc    └────┘                                                      └┘   └┘
txt    └────┘                                                      └┘   └┘
par    └────┘                                                      └┘   └┘
pid                                                               └┘   └┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
335  end
st   ──┘
336  
337  @[simp] lemma hom_of_cocone_of_hom {Y : C} (f : X ⟶ Y) : hom_of_cocone h (cocone_of_hom h f) = f :=
id                                                        └───────────┘   └───────────┘     
src                                                          └───────────┘    └───────────┘      
typ                                                       └───────────┘   └───────────┘     
doc    └──┘                                                   └───────────┘    └───────────┘
338  congr_fun (congr_fun (congr_arg nat_trans.app h.hom_inv_id) Y) f
id   └───────┘  └───────┘  └───────┘ └───────────┘ └─────────┘    
src  └───────┘  └───────┘  └───────┘ └───────────┘  └─────────┘
typ  └───────┘  └───────┘  └───────┘ └───────────┘ └─────────┘    
339  
340  /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X`
341  will be a colimit cocone. -/
342  def colimit_cocone : cocone F :=
id                        └────┘ 
src                       └────┘
typ                       └────┘ 
doc                       └────┘
343  cocone_of_hom h (𝟙 X)
id   └───────────┘    
src  └───────────┘    
typ  └───────────┘    
doc  └───────────┘
344  
345  /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
346  the colimit cocone extended by `f`. -/
347  lemma cocone_of_hom_fac {Y : C} (f : X ⟶ Y) :
id                                         
src                                         
typ                                        
348  cocone_of_hom h f = (colimit_cocone h).extend f :=
id   └───────────┘     └────────────┘  └────┘  
src  └───────────┘       └────────────┘   └────┘
typ  └───────────┘     └────────────┘  └────┘  
doc  └───────────┘        └────────────┘   └────┘
349  begin
st   └─────
350    dsimp [cocone_of_hom, colimit_cocone, cocone.extend],
id            └───────────┘  └────────────┘  └───────────┘
src    └─────┘└───────────┘└┘└────────────┘└┘└───────────┘
typ    └─────┘└───────────┘└┘└────────────┘└┘└───────────┘
doc    └─────┘└───────────┘└┘└────────────┘└┘└───────────┘
txt    └─────┘             └┘              └┘             
par    └─────┘             └┘              └┘             
pid                      └┘              └┘             
st   ─────────────────────────────────────────────────────┘└─
351    congr,
src    └───┘
typ    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
352    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
353    have t := congr_fun (h.hom.naturality f) (𝟙 X),
id               └───────┘  └──────────────┘     
src    └────────┘└───────┘ └──────────────┘ └┘  
typ    └────────┘└───────┘ └──────────────┘└┘ 
doc    └────────┘                           └┘   
txt    └────────┘                           └┘   
par    └────────┘                           └┘   
pid    └────┘└─┘                           └┘   
st   ───────────────────────────────────────────────┘└─
354    dsimp at t,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid         └──┘
st   ───────────┘└─
355    simp only [id_comp] at t,
id                └─────┘
src    └─────────┘└─────┘└────┘
typ    └─────────┘└─────┘└────┘
doc    └─────────┘       └────┘
txt    └─────────┘       └────┘
par    └─────────┘       └────┘
pid        └──┘└┘       └──┘
st   ─────────────────────────┘└─
356    rw congr_fun (congr_arg nat_trans.app t) j,
id        └───────┘  └───────┘ └───────────┘   
src    └─┘└───────┘ └───────┘└───────────┘ └┘
typ    └─┘└───────┘ └───────┘└───────────┘└┘
doc    └─┘                                 └┘
txt    └─┘                                 └┘
par    └─┘                                 └┘
pid                                       └┘
st   ───────────────────────────────────────────┘└─
357    refl,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
358  end
st   ──┘
359  
360  /-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
361  corresponding morphism. -/
362  lemma cocone_fac (s : cocone F) : (colimit_cocone h).extend (hom_of_cocone h s) = s :=
id                         └────┘      └────────────┘  └────┘   └───────────┘     
src                        └────┘       └────────────┘   └────┘   └───────────┘      
typ                        └────┘      └────────────┘  └────┘   └───────────┘     
doc                        └────┘       └────────────┘   └────┘   └───────────┘
363  begin
st   └─────
364    rw ←cocone_of_hom_of_cocone h s,
id         └─────────────────────┘  
src    └──┘└─────────────────────┘ 
typ    └──┘└─────────────────────┘
doc    └──┘                        
txt    └──┘                        
par    └──┘                        
pid      └┘                        
st   ────────────────────────────────┘└─
365    conv_lhs { simp only [hom_of_cocone_of_hom] },
id                           └──────────────────┘
src    └─────────┘└─────────┘└──────────────────┘└┘
typ    └─────────┘└─────────┘└──────────────────┘└┘
txt    └─────────┘└─────────┘                    └┘
par    └─────────┘└─────────┘                    └┘
pid            └───────────┘                    └─┘
st   ───────────┘└────────────────────────────────┘└┘
366    apply (cocone_of_hom_fac _ _).symm,
id            └───────────────┘
src    └────┘ └───────────────┘└────────┘
typ    └────┘ └───────────────┘└────────┘
doc    └────┘ └───────────────┘└────────┘
txt    └────┘                  └────────┘
par    └────┘                  └────────┘
pid                           └───────┘
st   ───────────────────────────────────┘└─
367  end
st   ──┘
368  
369  end of_nat_iso
370  
371  section
372  open of_nat_iso
373  
374  /--
375  If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on
376  the representing object is a colimit cocone.
377  -/
378  def of_nat_iso {X : C} (h : coyoneda.obj (op X) ≅ F.cocones) :
id                              └──────┘└──┘  └┘    └──────┘
src                              └──────┘└──┘  └┘      └──────┘
typ                             └──────┘└──┘  └┘    └──────┘
doc                                                     └──────┘
379    is_colimit (colimit_cocone h) :=
id     └────────┘  └────────────┘ 
src    └────────┘  └────────────┘
typ    └────────┘  └────────────┘ 
doc    └────────┘  └────────────┘
380  { desc := λ s, hom_of_cocone h s,
id                 └───────────┘  
src                 └───────────┘
typ                └───────────┘  
doc                 └───────────┘
381    fac' := λ s j,
id                
typ               
382    begin
st     └─────
383      have h := cocone_fac h s,
id                 └────────┘  
src      └────────┘└────────┘ 
typ      └────────┘└────────┘
doc      └────────┘└────────┘ 
txt      └────────┘           
par      └────────┘           
pid      └────┘└─┘           
st   ───────────────────────────┘└─
384      cases s,
id             
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────┘└─
385      injection h with h₁ h₂,
id                 
src      └────────┘ └─────────┘
typ      └────────┘└─────────┘
doc      └────────┘ └─────────┘
txt      └────────┘ └─────────┘
par      └────────┘ └─────────┘
pid                └─────────┘
st   ─────────────────────────┘└─
386      simp only [heq_iff_eq] at h₂,
id                  └────────┘
src      └─────────┘└────────┘└─────┘
typ      └─────────┘└────────┘└─────┘
doc      └─────────┘          └─────┘
txt      └─────────┘          └─────┘
par      └─────────┘          └─────┘
pid          └──┘└┘          └───┘
st   ───────────────────────────────┘└─
387      conv_rhs { rw ← h₂ }, refl,
id                       └┘
src      └─────────┘└───┘    └──┘
typ      └─────────┘└───┘└┘  └──┘
doc                            └──┘
txt      └─────────┘└───┘    └──┘
par      └─────────┘└───┘    └──┘
pid              └─────┘  └┘
st   ─────────────┘└───────┘└┘└───┘└─
388    end,
st   ────┘
389    uniq' := λ s m w,
id                  
typ                 
390    begin
st     └─────
391      rw ←hom_of_cocone_of_hom h m,
id           └──────────────────┘  
src      └──┘└──────────────────┘ 
typ      └──┘└──────────────────┘
doc      └──┘                     
txt      └──┘                     
par      └──┘                     
pid        └┘                     
st   ───────────────────────────────┘└─
392      congr,
src      └───┘
typ      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
393      rw cocone_of_hom_fac,
id          └───────────────┘
src      └─┘└───────────────┘
typ      └─┘└───────────────┘
doc      └─┘└───────────────┘
txt      └─┘
par      └─┘
pid        
st   ───────────────────────┘└─
394      dsimp, cases s, congr,
id                    
src      └───┘  └────┘   └───┘
typ      └───┘  └────┘  └───┘
doc      └───┘  └────┘
txt      └───┘  └────┘   └───┘
par      └───┘  └────┘   └───┘
pid                  
st   ────────┘└───────┘└─────┘└─
395      ext j, exact w j,
id                     
src      └───┘  └────┘ 
typ      └───┘  └────┘
doc      └───┘  └────┘ 
txt      └───┘  └────┘ 
par      └───┘  └────┘ 
pid         └┘        
st   ────────┘└─────────┘└─
396    end }
st   ────┘
397  end
398  
399  end is_colimit
400  
401  section limit
402  
403  /-- `has_limit F` represents a particular chosen limit of the diagram `F`. -/
404  class has_limit (F : J ⥤ C) :=
id                          
src                         
typ                         
doc                         
405  (cone : cone F)
id           └──┘ 
src          └──┘
typ          └──┘ 
doc          └──┘
406  (is_limit : is_limit cone . tactic.apply_instance)
id               └──────┘ └──┘ 
src              └──────┘
typ              └──────┘ └──┘ 
doc              └──────┘
407  
408  variables (J C)
409  
410  /-- `C` has limits of shape `J` if we have chosen a particular limit of
411    every functor `F : J ⥤ C`. -/
412  class has_limits_of_shape :=
413  (has_limit : Π F : J ⥤ C, has_limit F)
id                         └───────┘ 
src                           └───────┘
typ                        └───────┘ 
doc                           └───────┘
414  
415  /-- `C` has all (small) limits if it has limits of every shape. -/
416  class has_limits :=
417  (has_limits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C)
id                                └──┘         └────────────┘    └─────────────────┘  
src                                             └────────────┘     └─────────────────┘
typ                               └──┘         └────────────┘    └─────────────────┘  
doc                                             └────────────┘     └─────────────────┘
418  
419  variables {J C}
420  
421  @[priority 100] -- see Note [lower instance priority]
422  instance has_limit_of_has_limits_of_shape
423    {J : Type v} [small_category J] [H : has_limits_of_shape J C] (F : J ⥤ C) : has_limit F :=
id                   └────────────┘        └─────────────────┘               └───────┘ 
src                  └────────────┘         └─────────────────┘                   └───────┘
typ                  └────────────┘        └─────────────────┘               └───────┘ 
doc                  └────────────┘         └─────────────────┘                   └───────┘
424  has_limits_of_shape.has_limit F
id   └───────────────────────────┘ 
src  └───────────────────────────┘
typ  └───────────────────────────┘ 
425  
426  @[priority 100] -- see Note [lower instance priority]
427  instance has_limits_of_shape_of_has_limits
428    {J : Type v} [small_category J] [H : has_limits.{v} C] : has_limits_of_shape J C :=
id                   └────────────┘        └────────┘         └─────────────────┘  
src                  └────────────┘         └────────┘          └─────────────────┘
typ                  └────────────┘        └────────┘         └─────────────────┘  
doc                  └────────────┘         └────────┘          └─────────────────┘
429  has_limits.has_limits_of_shape C J
id   └────────────────────────────┘  
src  └────────────────────────────┘
typ  └────────────────────────────┘  
430  
431  /- Interface to the `has_limit` class. -/
432  
433  def limit.cone (F : J ⥤ C) [has_limit F] : cone F := has_limit.cone F
id                            └───────┘     └──┘     └────────────┘ 
src                             └───────┘      └──┘      └────────────┘
typ                           └───────┘     └──┘     └────────────┘ 
doc                             └───────┘      └──┘
434  
435  def limit (F : J ⥤ C) [has_limit F] := (limit.cone F).X
id                       └───────┘       └────────┘  
src                        └───────┘        └────────┘   
typ                      └───────┘       └────────┘  
doc                        └───────┘
436  
437  def limit.π (F : J ⥤ C) [has_limit F] (j : J) : limit F ⟶ F.obj j :=
id                         └───────┘            └───┘   └──┘ 
src                          └───────┘              └───┘     └──┘
typ                        └───────┘            └───┘   └──┘ 
doc                          └───────┘
438  (limit.cone F).π.app j
id    └────────┘   └─┘  
src   └────────┘    └─┘
typ   └────────┘   └─┘  
439  
440  @[simp] lemma limit.cone_π {F : J ⥤ C} [has_limit F] (j : J) :
id                                        └───────┘        
src                                         └───────┘
typ                                       └───────┘        
doc    └──┘                                 └───────┘
441    (limit.cone F).π.app j = limit.π _ j := rfl
id      └────────┘   └─┘    └─────┘       └─┘
src     └────────┘    └─┘     └─────┘        └─┘
typ     └────────┘   └─┘    └─────┘       └─┘
442  
443  @[simp] lemma limit.w (F : J ⥤ C) [has_limit F] {j j' : J} (f : j ⟶ j') :
id                                   └───────┘                    └┘
src                                    └───────┘                      
typ                                  └───────┘                    └┘
doc    └──┘                            └───────┘
444    limit.π F j ≫ F.map f = limit.π F j' := (limit.cone F).w f
id     └─────┘    └──┘   └─────┘  └┘     └────────┘    
src    └─────┘       └──┘    └─────┘          └────────┘   
typ    └─────┘    └──┘   └─────┘  └┘     └────────┘    
445  
446  def limit.is_limit (F : J ⥤ C) [has_limit F] : is_limit (limit.cone F) :=
id                                └───────┘     └──────┘  └────────┘ 
src                                 └───────┘      └──────┘  └────────┘
typ                               └───────┘     └──────┘  └────────┘ 
doc                                 └───────┘      └──────┘
447  has_limit.is_limit.{v} F
id   └────────────────┘     
src  └────────────────┘
typ  └────────────────┘     
448  
449  def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
id                            └───────┘        └──┘     └┘  └───┘ 
src                             └───────┘         └──┘       └┘  └───┘
typ                           └───────┘        └──┘     └┘  └───┘ 
doc                             └───────┘         └──┘
450  (limit.is_limit F).lift c
id    └────────────┘  └──┘  
src   └────────────┘   └──┘
typ   └────────────┘  └──┘  
451  
452  @[simp] lemma limit.is_limit_lift {F : J ⥤ C} [has_limit F] (c : cone F) :
id                                               └───────┘        └──┘ 
src                                                └───────┘         └──┘
typ                                              └───────┘        └──┘ 
doc    └──┘                                        └───────┘         └──┘
453    (limit.is_limit F).lift c = limit.lift F c := rfl
id      └────────────┘  └──┘    └────────┘      └─┘
src     └────────────┘   └──┘     └────────┘        └─┘
typ     └────────────┘  └──┘    └────────┘      └─┘
454  
455  @[simp, reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
id                                                 └───────┘        └──┘        
src                                                  └───────┘         └──┘
typ                                                └───────┘        └──┘        
doc    └──┘  └─────┘                                 └───────┘         └──┘
456    limit.lift F c ≫ limit.π F j = c.π.app j :=
id     └────────┘    └─────┘    └┘└──┘ 
src    └────────┘      └─────┘       └┘└──┘
typ    └────────┘    └─────┘    └┘└──┘ 
457  is_limit.fac _ c j
id   └──────────┘    
typ  └──────────┘    
458  
459  def limit.cone_morphism {F : J ⥤ C} [has_limit F] (c : cone F) :
id                                     └───────┘        └──┘ 
src                                      └───────┘         └──┘
typ                                    └───────┘        └──┘ 
doc                                      └───────┘         └──┘
460    cone_morphism c (limit.cone F) :=
id     └───────────┘   └────────┘ 
src    └───────────┘    └────────┘
typ    └───────────┘   └────────┘ 
461  (limit.is_limit F).lift_cone_morphism c
id    └────────────┘  └────────────────┘  
src   └────────────┘   └────────────────┘
typ   └────────────┘  └────────────────┘  
462  
463  @[simp] lemma limit.cone_morphism_hom {F : J ⥤ C} [has_limit F] (c : cone F) :
id                                                   └───────┘        └──┘ 
src                                                    └───────┘         └──┘
typ                                                  └───────┘        └──┘ 
doc    └──┘                                            └───────┘         └──┘
464    (limit.cone_morphism c).hom = limit.lift F c := rfl
id      └─────────────────┘  └─┘   └────────┘      └─┘
src     └─────────────────┘   └─┘   └────────┘        └─┘
typ     └─────────────────┘  └─┘   └────────┘      └─┘
465  @[simp] lemma limit.cone_morphism_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
id                                                 └───────┘        └──┘        
src                                                  └───────┘         └──┘
typ                                                └───────┘        └──┘        
doc    └──┘                                          └───────┘         └──┘
466    (limit.cone_morphism c).hom ≫ limit.π F j = c.π.app j :=
id      └─────────────────┘  └─┘   └─────┘    └┘└──┘ 
src     └─────────────────┘   └─┘   └─────┘       └┘└──┘
typ     └─────────────────┘  └─┘   └─────┘    └┘└──┘ 
467  by erw is_limit.fac
id          └──────────┘
src     └──┘            
typ     └──┘└──────────┘
doc     └──┘            
txt     └──┘            
par     └──┘            
pid                    
st     └─────────────────
468  
src  
typ  
doc  
txt  
par  
pid  
st   
469  @[ext] lemma limit.hom_ext {F : J ⥤ C} [has_limit F] {X : C} {f f' : X ⟶ limit F}
id                                        └───────┘                    └───┘ 
src                                         └───────┘                       └───┘
typ                                       └───────┘                    └───┘ 
doc    └─┘                                  └───────┘
470    (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
id                └─────┘    └┘  └─────┘        └┘
src                 └─────┘          └─────┘          
typ               └─────┘    └┘  └─────┘        └┘
471  (limit.is_limit F).hom_ext w
id    └────────────┘  └─────┘  
src   └────────────┘   └─────┘
typ   └────────────┘  └─────┘  
doc                    └─────┘
472  
473  def limit.hom_iso (F : J ⥤ C) [has_limit F] (W : C) : (W ⟶ limit F) ≅ (F.cones.obj (op W)) :=
id                               └───────┘               └───┘     └────┘└──┘  └┘ 
src                                └───────┘                  └───┘       └────┘└──┘  └┘
typ                              └───────┘               └───┘     └────┘└──┘  └┘ 
doc                                └───────┘                                └────┘
474  (limit.is_limit F).hom_iso W
id    └────────────┘  └─────┘  
src   └────────────┘   └─────┘
typ   └────────────┘  └─────┘  
doc                    └─────┘
475  
476  @[simp] lemma limit.hom_iso_hom (F : J ⥤ C) [has_limit F] {W : C} (f : W ⟶ limit F) :
id                                             └───────┘                 └───┘ 
src                                              └───────┘                    └───┘
typ                                            └───────┘                 └───┘ 
doc    └──┘                                      └───────┘
477    (limit.hom_iso F W).hom f = (const J).map f ≫ (limit.cone F).π :=
id      └───────────┘   └─┘     └───┘  └─┘     └────────┘  
src     └───────────┘     └─┘      └───┘   └─┘      └────────┘   
typ     └───────────┘   └─┘     └───┘  └─┘     └────────┘  
478  (limit.is_limit F).hom_iso_hom f
id    └────────────┘  └─────────┘  
src   └────────────┘   └─────────┘
typ   └────────────┘  └─────────┘  
479  
480  def limit.hom_iso' (F : J ⥤ C) [has_limit F] (W : C) :
id                                └───────┘        
src                                 └───────┘
typ                               └───────┘        
doc                                 └───────┘
481    ((W ⟶ limit F) : Type v) ≅ { p : Π j, W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
id         └───┘                         └──┘                        └┘      └──┘    └┘
src         └───┘                             └──┘                                      └──┘   
typ        └───┘                         └──┘                        └┘      └──┘    └┘
482  (limit.is_limit F).hom_iso' W
id    └────────────┘  └──────┘  
src   └────────────┘   └──────┘
typ   └────────────┘  └──────┘  
483  
484  lemma limit.lift_extend {F : J ⥤ C} [has_limit F] (c : cone F) {X : C} (f : X ⟶ c.X) :
id                                     └───────┘        └──┘                 └┘
src                                      └───────┘         └──┘                     └┘
typ                                    └───────┘        └──┘                 └┘
doc                                      └───────┘         └──┘
485    limit.lift F (c.extend f) = f ≫ limit.lift F c :=
id     └────────┘   └─────┘      └────────┘  
src    └────────┘     └─────┘        └────────┘
typ    └────────┘   └─────┘      └────────┘  
doc                   └─────┘
486  by obviously
id      └───────┘
src     └───────┘
typ     └───────┘
doc     └───────┘
par     └───────┘
st     └────────┘
487  
488  def has_limit_of_iso {F G : J ⥤ C} [has_limit F] (α : F ≅ G) : has_limit G :=
id                                    └───────┘              └───────┘ 
src                                     └───────┘                 └───────┘
typ                                   └───────┘              └───────┘ 
doc                                     └───────┘                  └───────┘
489  { cone := (cones.postcompose α.hom).obj (limit.cone F),
id              └───────────────┘ └──┘ └─┘   └────────┘ 
src             └───────────────┘  └──┘ └─┘   └────────┘
typ             └───────────────┘ └──┘ └─┘   └────────┘ 
490    is_limit :=
491    { lift := λ s, limit.lift F ((cones.postcompose α.inv).obj s),
id                   └────────┘    └───────────────┘ └──┘ └─┘  
src                   └────────┘     └───────────────┘  └──┘ └─┘
typ                  └────────┘    └───────────────┘ └──┘ └─┘  
492      fac' := λ s j,
id                  
typ                 
493      begin
st       └─────
494        rw [cones.postcompose_obj_π, nat_trans.comp_app, limit.cone_π, ←category.assoc, limit.lift_π],
id             └─────────────────────┘  └────────────────┘  └──────────┘   └────────────┘  └──────────┘
src        └──┘└─────────────────────┘└┘└────────────────┘└┘└──────────┘└─┘└────────────┘└┘└──────────┘
typ        └──┘└─────────────────────┘└┘└────────────────┘└┘└──────────┘└─┘└────────────┘└┘└──────────┘
doc        └──┘                       └┘                  └┘            └─┘              └┘            
txt        └──┘                       └┘                  └┘            └─┘              └┘            
par        └──┘                       └┘                  └┘            └─┘              └┘            
pid          └┘                       └┘                  └┘            └─┘              └┘            
st   ────────────────────────────────┘└──────────────────┘└────────────┘└───────────────┘└────────────┘└──
495        simp
src        └────
typ        └────
doc        └────
txt        └────
par        └────
pid            
st   ───────────
496      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
497      uniq' := λ s m w,
id                    
typ                   
498      begin
st       └─────
499        apply limit.hom_ext, intro j,
id               └───────────┘
src        └────┘└───────────┘  └─────┘
typ        └────┘└───────────┘  └─────┘
doc        └────┘               └─────┘
txt        └────┘               └─────┘
par        └────┘               └─────┘
pid                                 └┘
st   ────────────────────────┘└───────┘└─
500        rw [limit.lift_π, cones.postcompose_obj_π, nat_trans.comp_app, ←nat_iso.app_inv, iso.eq_comp_inv],
id             └──────────┘  └─────────────────────┘  └────────────────┘   └─────────────┘  └─────────────┘
src        └──┘└──────────┘└┘└─────────────────────┘└┘└────────────────┘└─┘└─────────────┘└┘└─────────────┘
typ        └──┘└──────────┘└┘└─────────────────────┘└┘└────────────────┘└─┘└─────────────┘└┘└─────────────┘
doc        └──┘            └┘                       └┘                  └─┘               └┘               
txt        └──┘            └┘                       └┘                  └─┘               └┘               
par        └──┘            └┘                       └┘                  └─┘               └┘               
pid          └┘            └┘                       └┘                  └─┘               └┘               
st   ─────────────────────┘└───────────────────────┘└──────────────────┘└────────────────┘└───────────────┘└──
501        simpa using w j
id                      
src        └──────────┘  
typ        └──────────┘
doc        └──────────┘  
txt        └──────────┘  
par        └──────────┘  
pid             └────┘  
st   ──────────────────────
502      end } }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
503  
504  /-- If a functor `G` has the same collection of cones as a functor `F`
505  which has a limit, then `G` also has a limit. -/
506  -- See the construction of limits from products and equalizers
507  -- for an example usage.
508  def has_limit.of_cones_iso {J K : Type v} [small_category J] [small_category K] (F : J ⥤ C) (G : K ⥤ C)
id                                              └────────────┘    └────────────┘                   
src                                             └────────────┘     └────────────┘                      
typ                                             └────────────┘    └────────────┘                   
doc                                             └────────────┘     └────────────┘                      
509    (h : F.cones ≅ G.cones) [has_limit F] : has_limit G :=
id          └────┘  └────┘   └───────┘     └───────┘ 
src          └────┘   └────┘   └───────┘      └───────┘
typ         └────┘  └────┘   └───────┘     └───────┘ 
doc          └────┘    └────┘   └───────┘      └───────┘
510  ⟨_, is_limit.of_nat_iso ((is_limit.nat_iso (limit.is_limit F)) ≪≫ h)⟩
id       └─────────────────┘   └──────────────┘  └────────────┘    └┘ 
src      └─────────────────┘   └──────────────┘  └────────────┘     └┘
typ      └─────────────────┘   └──────────────┘  └────────────┘    └┘ 
doc      └─────────────────┘   └──────────────┘
511  
512  section pre
513  variables (F) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)]
id                  └───────┘                └───────┘    
src                 └───────┘                └───────┘    
typ                 └───────┘                └───────┘    
doc                 └───────┘                └───────┘    
514  
515  def limit.pre : limit F ⟶ limit (E ⋙ F) :=
id                   └───┘   └───┘    
src                  └───┘    └───┘    
typ                  └───┘   └───┘    
doc                                     
516  limit.lift (E ⋙ F)
id   └────────┘    
src  └────────┘    
typ  └────────┘    
doc                
517    { X := limit F,
id            └───┘ 
src           └───┘
typ           └───┘ 
518      π := { app := λ k, limit.π F (E.obj k) } }
id                        └─────┘   └──┘ 
src                        └─────┘     └──┘
typ                       └─────┘   └──┘ 
doc           
519  
520  @[simp] lemma limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
id                                      └───────┘    └─────┘        └─────┘   └──┘ 
src                                      └───────┘      └─────┘           └─────┘     └──┘
typ                                     └───────┘    └─────┘        └─────┘   └──┘ 
doc    └──┘                                                         
521  by erw is_limit.fac
id          └──────────┘
src     └──┘            
typ     └──┘└──────────┘
doc     └──┘            
txt     └──┘            
par     └──┘            
pid                    
st     └─────────────────
522  
src  
typ  
doc  
txt  
par  
pid  
st   
523  @[simp] lemma limit.lift_pre (c : cone F) :
id                                     └──┘ 
src                                    └──┘
typ                                    └──┘ 
doc    └──┘                            └──┘
524    limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E) :=
id     └────────┘    └───────┘    └────────┘       └──────┘ 
src    └────────┘      └───────┘      └────────┘          └──────┘
typ    └────────┘    └───────┘    └────────┘       └──────┘ 
doc                                                   
525  by ext; simp
src     └─┘  └────
typ     └─┘  └────
doc     └─┘  └────
txt     └─┘  └────
par     └─┘  └────
pid              
st     └──────────
526  
src  
typ  
doc  
txt  
par  
pid  
st   
527  variables {L : Type v} [small_category L]
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
doc                          └────────────┘
528  variables (D : L ⥤ K) [has_limit (D ⋙ E ⋙ F)]
id                         └───────┘       
src                        └───────┘       
typ                        └───────┘       
doc                        └───────┘       
529  
530  @[simp] lemma limit.pre_pre : limit.pre F E ≫ limit.pre (E ⋙ F) D = limit.pre F (D ⋙ E) :=
id                                 └───────┘    └───────┘        └───────┘     
src                                └───────┘      └───────┘           └───────┘      
typ                                └───────┘    └───────┘        └───────┘     
doc    └──┘                                                                            
531  by ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; refl
id                  └───┘  └─────────┘  └─────────┘  └─────────┘
src     └───┘  └───┘└───┘└┘└─────────┘└┘└─────────┘└┘└─────────┘  └────
typ     └───┘  └───┘└───┘└┘└─────────┘└┘└─────────┘└┘└─────────┘  └────
doc     └───┘  └───┘     └┘           └┘           └┘             └────
txt     └───┘  └───┘     └┘           └┘           └┘             └────
par     └───┘  └───┘     └┘           └┘           └┘             └────
pid        └┘     └┘     └┘           └┘           └┘                 
st     └───────────┘└───┘└───────────┘└───────────┘└───────────┘└──────
532  
src  
typ  
doc  
txt  
par  
pid  
st   
533  end pre
534  
535  section post
536  variables {D : Type u'} [𝒟 : category.{v} D]
id                                └──────┘
src                               └──────┘
typ                               └──────┘
doc                               └──────┘
537  include 𝒟
538  
539  variables (F) [has_limit F] (G : C ⥤ D) [has_limit (F ⋙ G)]
id                  └───────┘                └───────┘    
src                 └───────┘                └───────┘    
typ                 └───────┘                └───────┘    
doc                 └───────┘                └───────┘    
540  
541  def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
id                    └──┘  └───┘    └───┘    
src                    └──┘  └───┘     └───┘    
typ                   └──┘  └───┘    └───┘    
doc                                              
542  limit.lift (F ⋙ G)
id   └────────┘    
src  └────────┘    
typ  └────────┘    
doc                
543  { X := G.obj (limit F),
id          └──┘  └───┘ 
src          └──┘  └───┘
typ         └──┘  └───┘ 
544    π :=
545    { app := λ j, G.map (limit.π F j),
id                  └──┘  └─────┘  
src                   └──┘  └─────┘
typ                 └──┘  └─────┘  
546      naturality' :=
547        by intros j j' f; erw [←G.map_comp, limits.cone.w, id_comp]; refl } }
id                                             └───────────┘  └─────┘
src           └───────────┘  └────┘          └┘└───────────┘└┘└─────┘  └───┘
typ           └───────────┘  └────┘└────────┘└┘└───────────┘└┘└─────┘  └───┘
doc           └───────────┘  └────┘          └┘             └┘         └───┘
txt           └───────────┘  └────┘          └┘             └┘         └───┘
par           └───────────┘  └────┘          └┘             └┘         └───┘
pid                 └─────┘     └─┘          └┘             └┘             
st           └───────────────────┘└─────────┘└─────────────┘└───────┘└─────┘
548  
549  @[simp] lemma limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) :=
id                                       └────────┘    └─────┘        └──┘  └─────┘  
src                                       └────────┘      └─────┘            └──┘  └─────┘
typ                                      └────────┘    └─────┘        └──┘  └─────┘  
doc    └──┘                                                           
550  by erw is_limit.fac
id          └──────────┘
src     └──┘            
typ     └──┘└──────────┘
doc     └──┘            
txt     └──┘            
par     └──┘            
pid                    
st     └─────────────────
551  
src  
typ  
doc  
txt  
par  
pid  
st   
552  @[simp] lemma limit.lift_post (c : cone F) :
id                                      └──┘ 
src                                     └──┘
typ                                     └──┘ 
doc    └──┘                             └──┘
553    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.map_cone c) :=
id     └──┘  └────────┘     └────────┘    └────────┘       └───────┘ 
src     └──┘  └────────┘       └────────┘      └────────┘          └───────┘
typ    └──┘  └────────┘     └────────┘    └────────┘       └───────┘ 
doc                                                                  └───────┘
554  by ext; rw [assoc, limit.post_π, ←G.map_comp, limit.lift_π, limit.lift_π]; refl
id               └───┘  └──────────┘               └──────────┘  └──────────┘
src     └─┘  └──┘└───┘└┘└──────────┘└─┘          └┘└──────────┘└┘└──────────┘  └────
typ     └─┘  └──┘└───┘└┘└──────────┘└─┘└────────┘└┘└──────────┘└┘└──────────┘  └────
doc     └─┘  └──┘     └┘            └─┘          └┘            └┘              └────
txt     └─┘  └──┘     └┘            └─┘          └┘            └┘              └────
par     └─┘  └──┘     └┘            └─┘          └┘            └┘              └────
pid            └┘     └┘            └─┘          └┘            └┘                  
st     └────────┘└───┘└────────────┘└───────────┘└────────────┘└────────────┘└──────
555  
src  
typ  
doc  
txt  
par  
pid  
st   
556  @[simp] lemma limit.post_post
doc    └──┘
557    {E : Type u''} [category.{v} E] (H : D ⥤ E) [has_limit ((F ⋙ G) ⋙ H)] :
id                     └──────┘                 └───────┘        
src                    └──────┘                    └───────┘         
typ                    └──────┘                 └───────┘        
doc                    └──────┘                    └───────┘         
558  /- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals -/
559  /- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H)) -/
560    H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H) :=
id     └──┘  └────────┘     └────────┘        └────────┘     
src     └──┘  └────────┘       └────────┘           └────────┘      
typ    └──┘  └────────┘     └────────┘        └────────┘     
doc                                                                   
561  by ext; erw [assoc, limit.post_π, ←H.map_comp, limit.post_π, limit.post_π]; refl
id                └───┘  └──────────┘               └──────────┘  └──────────┘
src     └─┘  └───┘└───┘└┘└──────────┘└─┘          └┘└──────────┘└┘└──────────┘  └────
typ     └─┘  └───┘└───┘└┘└──────────┘└─┘└────────┘└┘└──────────┘└┘└──────────┘  └────
doc     └─┘  └───┘     └┘            └─┘          └┘            └┘              └────
txt     └─┘  └───┘     └┘            └─┘          └┘            └┘              └────
par     └─┘  └───┘     └┘            └─┘          └┘            └┘              └────
pid             └┘     └┘            └─┘          └┘            └┘                  
st     └─────────┘└───┘└────────────┘└───────────┘└────────────┘└────────────┘└──────
562  
src  
typ  
doc  
txt  
par  
pid  
st   
563  end post
564  
565  lemma limit.pre_post {D : Type u'} [category.{v} D]
id                                       └──────┘     
src                                      └──────┘
typ                                      └──────┘     
doc                                      └──────┘
566    (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
id                              
src                                 
typ                             
doc                                 
567    [has_limit F] [has_limit (E ⋙ F)] [has_limit (F ⋙ G)] [has_limit ((E ⋙ F) ⋙ G)] :
id      └───────┘    └───────┘        └───────┘        └───────┘        
src     └───────┘     └───────┘          └───────┘          └───────┘         
typ     └───────┘    └───────┘        └───────┘        └───────┘        
doc     └───────┘     └───────┘          └───────┘          └───────┘         
568  /- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs -/
569  /- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or -/
570    G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E :=
id     └──┘  └───────┘     └────────┘        └────────┘    └───────┘      
src     └──┘  └───────┘       └────────┘           └────────┘      └───────┘    
typ    └──┘  └───────┘     └────────┘        └────────┘    └───────┘      
doc                                                                                
571  by ext; erw [assoc, limit.post_π, ←G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]; refl
id                └───┘  └──────────┘               └─────────┘  └───┘  └─────────┘  └──────────┘
src     └─┘  └───┘└───┘└┘└──────────┘└─┘          └┘└─────────┘└┘└───┘└┘└─────────┘└┘└──────────┘  └────
typ     └─┘  └───┘└───┘└┘└──────────┘└─┘└────────┘└┘└─────────┘└┘└───┘└┘└─────────┘└┘└──────────┘  └────
doc     └─┘  └───┘     └┘            └─┘          └┘           └┘     └┘           └┘              └────
txt     └─┘  └───┘     └┘            └─┘          └┘           └┘     └┘           └┘              └────
par     └─┘  └───┘     └┘            └─┘          └┘           └┘     └┘           └┘              └────
pid             └┘     └┘            └─┘          └┘           └┘     └┘           └┘                  
st     └─────────┘└───┘└────────────┘└───────────┘└───────────┘└─────┘└───────────┘└────────────┘└──────
572  
src  
typ  
doc  
txt  
par  
pid  
st   
573  open category_theory.equivalence
574  instance has_limit_equivalence_comp (e : K ≌ J) [has_limit F] : has_limit (e.functor ⋙ F) :=
id                                                 └───────┘     └───────┘  └──────┘  
src                                                  └───────┘      └───────┘   └──────┘ 
typ                                                └───────┘     └───────┘  └──────┘  
doc                                                  └───────┘      └───────┘            
575  { cone := cone.whisker e.functor (limit.cone F),
id             └──────────┘ └──────┘  └────────┘ 
src            └──────────┘  └──────┘  └────────┘
typ            └──────────┘ └──────┘  └────────┘ 
576    is_limit :=
577    let e' := cones.postcompose (e.inv_fun_id_assoc F).hom in
id         └┘    └───────────────┘  └───────────────┘  └─┘
src              └───────────────┘   └───────────────┘   └─┘
typ        └┘    └───────────────┘  └───────────────┘  └─┘
578    { lift := λ s, limit.lift F (e'.obj (cone.whisker e.inverse s)),
id                   └────────┘   └┘└──┘  └──────────┘ └──────┘ 
src                   └────────┘      └──┘  └──────────┘  └──────┘
typ                  └────────┘   └┘└──┘  └──────────┘ └──────┘ 
579      fac' := λ s j,
id                  
typ                 
580      begin
st       └─────
581        dsimp, rw [limit.lift_π], dsimp [e'],
id                    └──────────┘          └┘
src        └───┘  └──┘└──────────┘  └─────┘  
typ        └───┘  └──┘└──────────┘  └─────┘└┘
doc        └───┘  └──┘              └─────┘  
txt        └───┘  └──┘              └─────┘  
par        └───┘  └──┘              └─────┘  
pid                 └┘                     
st   ──────────┘└────────────────┘└───────────┘└─
582        erw [inv_fun_id_assoc_hom_app, counit_functor, ←s.π.naturality, id_comp]
id              └──────────────────────┘  └────────────┘                   └─────┘
src        └───┘└──────────────────────┘└┘└────────────┘└─┘              └┘└─────┘└─
typ        └───┘└──────────────────────┘└┘└────────────┘└─┘└────────────┘└┘└─────┘└─
doc        └───┘                        └┘              └─┘              └┘       └─
txt        └───┘                        └┘              └─┘              └┘       └─
par        └───┘                        └┘              └─┘              └┘       └─
pid           └┘                        └┘              └─┘              └┘       
st   ──────────────────────────────────┘└──────────────┘└───────────────┘└───────┘
583      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
584      uniq' := λ s m w,
id                    
typ                   
585      begin
st       └─────
586        apply limit.hom_ext, intro j,
id               └───────────┘
src        └────┘└───────────┘  └─────┘
typ        └────┘└───────────┘  └─────┘
doc        └────┘               └─────┘
txt        └────┘               └─────┘
par        └────┘               └─────┘
pid                                 └┘
st   ────────────────────────┘└───────┘└─
587        erw [limit.lift_π, ←limit.w F (e.counit_iso.hom.app j)],
id              └──────────┘   └─────┘   └──────────────────┘ 
src        └───┘└──────────┘└─┘└─────┘  └──────────────────┘ └┘
typ        └───┘└──────────┘└─┘└─────┘ └──────────────────┘└┘
doc        └───┘            └─┘                              └┘
txt        └───┘            └─┘                              └┘
par        └───┘            └─┘                              └┘
pid           └┘            └─┘                              └┘
st   ──────────────────────┘└───────────────────────────────────┘└──
588        slice_lhs 1 2 { erw [w (e.inverse.obj j)] }, simp
id                                └───────────┘ 
src        └──────────────┘└───┘  └───────────┘ └─┘  └────
typ        └──────────────┘└───┘ └───────────┘└─┘  └────
doc        └──────────────┘                            └────
txt        └──────────────┘└───┘                └─┘  └────
par        └──────────────┘└───┘                └─┘  └────
pid                 └┘└───────┘                └──┘      
st   ────────────────────┘└───────────────────────┘ └┘└─────
589      end } }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
590  
591  local attribute [elab_simple] inv_fun_id_assoc -- not entirely sure why this is needed
id                                 └──────────────┘
src                                └──────────────┘
typ                                └──────────────┘
doc                   └─────────┘
592  def has_limit_of_equivalence_comp (e : K ≌ J) [has_limit (e.functor ⋙ F)] : has_limit F :=
id                                               └───────┘  └──────┘       └───────┘ 
src                                                └───────┘   └──────┘        └───────┘
typ                                              └───────┘  └──────┘       └───────┘ 
doc                                                └───────┘                   └───────┘
593  begin
st   └─────
594    haveI : has_limit (e.inverse ⋙ e.functor ⋙ F) := limits.has_limit_equivalence_comp e.symm,
id             └───────┘  └───────┘  └───────┘        └───────────────────────────────┘ └────┘
src    └──────┘└───────┘ └───────┘└───────┘  └───┘└───────────────────────────────┘└────┘
typ    └──────┘└───────┘ └───────┘└───────┘ └───┘└───────────────────────────────┘└────┘
doc    └──────┘└───────┘                     └───┘                                 
txt    └──────┘                               └───┘                                 
par    └──────┘                               └───┘                                 
pid         └┘                               └──┘                                 
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
595    apply has_limit_of_iso (e.inv_fun_id_assoc F),
id           └──────────────┘  └────────────────┘ 
src    └────┘└──────────────┘ └────────────────┘ 
typ    └────┘└──────────────┘ └────────────────┘
doc    └────┘                                    
txt    └────┘                                    
par    └────┘                                    
pid                                             
st   ──────────────────────────────────────────────┘└─
596  end
st   ──┘
597  
598  -- `has_limit_comp_equivalence` and `has_limit_of_comp_equivalence`
599  -- are proved in `category_theory/adjunction/limits.lean`.
600  
601  section lim_functor
602  
603  variables [has_limits_of_shape J C]
id              └─────────────────┘
src             └─────────────────┘
typ             └─────────────────┘
doc             └─────────────────┘
604  
605  /-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`. -/
606  def lim : (J ⥤ C) ⥤ C :=
id                   
src                   
typ                  
doc                   
607  { obj := λ F, limit F,
id               └───┘ 
src               └───┘
typ              └───┘ 
doc  
608    map := λ F G α, limit.lift G
id                  └────────┘ 
src                    └────────┘
typ                 └────────┘ 
609      { X := limit F,
id              └───┘ 
src             └───┘
typ             └───┘ 
610        π :=
611        { app := λ j, limit.π F j ≫ α.app j,
id                      └─────┘    └──┘ 
src                      └─────┘       └──┘
typ                     └─────┘    └──┘ 
612          naturality' := λ j j' f,
id                             └┘ 
typ                            └┘ 
613            by erw [id_comp, assoc, ←α.naturality, ←assoc, limit.w] } },
id                     └─────┘  └───┘                  └───┘  └─────┘
src               └───┘└─────┘└┘└───┘└─┘            └─┘└───┘└┘└─────┘└┘
typ               └───┘└─────┘└┘└───┘└─┘└──────────┘└─┘└───┘└┘└─────┘└┘
doc               └───┘       └┘     └─┘            └─┘     └┘       └┘
txt               └───┘       └┘     └─┘            └─┘     └┘       └┘
par               └───┘       └┘     └─┘            └─┘     └┘       └┘
pid                  └┘       └┘     └─┘            └─┘     └┘       
st               └───────────┘└─────┘└─────────────┘└──────┘└───────┘
614    map_comp' := λ F G H α β,
id                        
typ                       
615      by ext; erw [assoc, is_limit.fac, is_limit.fac, ←assoc, is_limit.fac, assoc]; refl }
id                    └───┘  └──────────┘  └──────────┘   └───┘  └──────────┘  └───┘
src         └─┘  └───┘└───┘└┘            └┘            └─┘└───┘└┘            └┘└───┘  └───┘
typ         └─┘  └───┘└───┘└┘└──────────┘└┘└──────────┘└─┘└───┘└┘└──────────┘└┘└───┘  └───┘
doc         └─┘  └───┘     └┘            └┘            └─┘     └┘            └┘       └───┘
txt         └─┘  └───┘     └┘            └┘            └─┘     └┘            └┘       └───┘
par         └─┘  └───┘     └┘            └┘            └─┘     └┘            └┘       └───┘
pid                 └┘     └┘            └┘            └─┘     └┘            └┘           
st         └─────────┘└─────────────────────────────────────────────────────────────┘└─────┘
616  
617  variables {F} {G : J ⥤ C} (α : F ⟶ G)
id                                   
src                                  
typ                                  
doc                       
618  
619  @[simp, reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
id                                             └─┘└──┘   └─────┘    └─────┘    └──┘ 
src                                             └─┘└──┘    └─────┘      └─────┘       └──┘
typ                                            └─┘└──┘   └─────┘    └─────┘    └──┘ 
doc    └──┘  └─────┘                            └─┘
620  by apply is_limit.fac
id            └──────────┘
src     └────┘            
typ     └────┘└──────────┘
doc     └────┘            
txt     └────┘            
par     └────┘            
pid                      
st     └───────────────────
621  
src  
typ  
doc  
txt  
par  
pid  
st   
622  @[simp] lemma limit.lift_map (c : cone F) :
id                                     └──┘ 
src                                    └──┘
typ                                    └──┘ 
doc    └──┘                            └──┘
623    limit.lift F c ≫ lim.map α = limit.lift G ((cones.postcompose α).obj c) :=
id     └────────┘    └─┘└──┘   └────────┘    └───────────────┘  └─┘  
src    └────────┘      └─┘└──┘    └────────┘     └───────────────┘   └─┘
typ    └────────┘    └─┘└──┘   └────────┘    └───────────────┘  └─┘  
doc                     └─┘
624  by ext; rw [assoc, lim.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
id               └───┘  └───────┘   └───┘  └──────────┘  └──────────┘
src     └─┘  └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘└┘└──────────┘  └────
typ     └─┘  └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘└┘└──────────┘  └────
doc     └─┘  └──┘     └┘         └─┘     └┘            └┘              └────
txt     └─┘  └──┘     └┘         └─┘     └┘            └┘              └────
par     └─┘  └──┘     └┘         └─┘     └┘            └┘              └────
pid            └┘     └┘         └─┘     └┘            └┘                  
st     └────────┘└───┘└─────────┘└──────┘└────────────┘└────────────┘└──────
625  
src  
typ  
doc  
txt  
par  
pid  
st   
626  lemma limit.map_pre [has_limits_of_shape K C] (E : K ⥤ J) :
id                        └─────────────────┘           
src                       └─────────────────┘             
typ                       └─────────────────┘           
doc                       └─────────────────┘             
627    lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whisker_left E α) :=
id     └─┘└──┘   └───────┘    └───────┘    └─┘└──┘  └──────────┘  
src    └─┘└──┘    └───────┘      └───────┘      └─┘└──┘  └──────────┘
typ    └─┘└──┘   └───────┘    └───────┘    └─┘└──┘  └──────────┘  
doc    └─┘                                         └─┘
628  by ext; rw [assoc, limit.pre_π, lim.map_π, assoc, lim.map_π, ←assoc, limit.pre_π]; refl
id               └───┘  └─────────┘  └───────┘  └───┘  └───────┘   └───┘  └─────────┘
src     └─┘  └──┘└───┘└┘└─────────┘└┘└───────┘└┘└───┘└┘└───────┘└─┘└───┘└┘└─────────┘  └────
typ     └─┘  └──┘└───┘└┘└─────────┘└┘└───────┘└┘└───┘└┘└───────┘└─┘└───┘└┘└─────────┘  └────
doc     └─┘  └──┘     └┘           └┘         └┘     └┘         └─┘     └┘             └────
txt     └─┘  └──┘     └┘           └┘         └┘     └┘         └─┘     └┘             └────
par     └─┘  └──┘     └┘           └┘         └┘     └┘         └─┘     └┘             └────
pid            └┘     └┘           └┘         └┘     └┘         └─┘     └┘                 
st     └────────┘└───┘└───────────┘└─────────┘└─────┘└─────────┘└──────┘└───────────┘└──────
629  
src  
typ  
doc  
txt  
par  
pid  
st   
630  lemma limit.map_pre' [has_limits_of_shape.{v} K C]
id                         └─────────────────┘      
src                        └─────────────────┘
typ                        └─────────────────┘      
doc                        └─────────────────┘
631    (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
id                                └┘  └┘
src                                      
typ                               └┘  └┘
doc                          
632    limit.pre F E₂ = limit.pre F E₁ ≫ lim.map (whisker_right α F) :=
id     └───────┘  └┘  └───────┘  └┘  └─┘└──┘  └───────────┘  
src    └───────┘       └───────┘       └─┘└──┘  └───────────┘
typ    └───────┘  └┘  └───────┘  └┘  └─┘└──┘  └───────────┘  
doc                                      └─┘
633  by ext1; simp [(category.assoc _ _ _ _).symm]
id                   └────────────┘
src     └──┘  └────┘ └────────────┘└───────────────
typ     └──┘  └────┘ └────────────┘└───────────────
doc     └──┘  └────┘               └───────────────
txt     └──┘  └────┘               └───────────────
par     └──┘  └────┘               └───────────────
pid                              └─────────────┘
st     └───────────────────────────────────────────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  lemma limit.id_pre (F : J ⥤ C) :
id                             
src                            
typ                            
doc                            
636  limit.pre F (𝟭 _) = lim.map (functor.left_unitor F).inv := by tidy
id   └───────┘        └─┘└──┘  └─────────────────┘  └─┘
src  └───────┘         └─┘└──┘  └─────────────────┘   └─┘        └────
typ  └───────┘        └─┘└──┘  └─────────────────┘  └─┘        └────
doc                     └─┘                                       └────
txt                                                                └────
par                                                                └────
pid                                                                    
st                                                                └─────
637  
src  
typ  
doc  
txt  
par  
pid  
st   
638  lemma limit.map_post {D : Type u'} [category.{v} D] [has_limits_of_shape J D] (H : C ⥤ D) :
id                                       └──────┘        └─────────────────┘           
src                                      └──────┘         └─────────────────┘             
typ                                      └──────┘        └─────────────────┘           
doc                                      └──────┘         └─────────────────┘             
639  /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
640     H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
641    H.map (lim.map α) ≫ limit.post G H = limit.post F H ≫ lim.map (whisker_right α H) :=
id     └──┘  └─┘└──┘    └────────┘    └────────┘    └─┘└──┘  └───────────┘  
src     └──┘  └─┘└──┘     └────────┘      └────────┘      └─┘└──┘  └───────────┘
typ    └──┘  └─┘└──┘    └────────┘    └────────┘    └─┘└──┘  └───────────┘  
doc           └─┘                                            └─┘
642  begin
st   └─────
643    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
644    rw [assoc, limit.post_π, ←H.map_comp, lim.map_π, H.map_comp],
id         └───┘  └──────────┘               └───────┘
src    └──┘└───┘└┘└──────────┘└─┘          └┘└───────┘└┘          
typ    └──┘└───┘└┘└──────────┘└─┘└────────┘└┘└───────┘└┘└────────┘
doc    └──┘     └┘            └─┘          └┘         └┘          
txt    └──┘     └┘            └─┘          └┘         └┘          
par    └──┘     └┘            └─┘          └┘         └┘          
pid      └┘     └┘            └─┘          └┘         └┘          
st   ──────────┘└────────────┘└───────────┘└─────────┘└──────────┘└──
645    rw [assoc, lim.map_π, ←assoc, limit.post_π],
id         └───┘  └───────┘   └───┘  └──────────┘
src    └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘
typ    └──┘└───┘└┘└───────┘└─┘└───┘└┘└──────────┘
doc    └──┘     └┘         └─┘     └┘            
txt    └──┘     └┘         └─┘     └┘            
par    └──┘     └┘         └─┘     └┘            
pid      └┘     └┘         └─┘     └┘            
st   ──────────┘└─────────┘└──────┘└────────────┘└──
646    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
647  end
st   └─┘
648  
649  def lim_yoneda : lim ⋙ yoneda ≅ category_theory.cones J C :=
id                    └─┘  └────┘  └───────────────────┘  
src                   └─┘  └────┘  └───────────────────┘
typ                   └─┘  └────┘  └───────────────────┘  
doc                   └─┘           └───────────────────┘
650  nat_iso.of_components (λ F, nat_iso.of_components (λ W, limit.hom_iso F (unop W)) (by tidy))
id   └───────────────────┘      └───────────────────┘      └───────────┘   └──┘ 
src  └───────────────────┘       └───────────────────┘       └───────────┘    └──┘         └──┘
typ  └───────────────────┘      └───────────────────┘      └───────────┘   └──┘        └──┘
doc                                                                                        └──┘
txt                                                                                        └──┘
par                                                                                        └──┘
st                                                                                        └───┘
651    (by tidy)
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st        └───┘
652  
653  end lim_functor
654  
655  def has_limits_of_shape_of_equivalence {J' : Type v} [small_category J']
id                                                         └────────────┘ └┘
src                                                        └────────────┘
typ                                                        └────────────┘ └┘
doc                                                        └────────────┘
656    (e : J ≌ J') [has_limits_of_shape J C] : has_limits_of_shape J' C :=
id            └┘   └─────────────────┘      └─────────────────┘ └┘ 
src                 └─────────────────┘        └─────────────────┘
typ           └┘   └─────────────────┘      └─────────────────┘ └┘ 
doc                 └─────────────────┘        └─────────────────┘
657  by { constructor, intro F, apply has_limit_of_equivalence_comp e, apply_instance }
id                                    └───────────────────────────┘ 
src       └─────────┘  └─────┘  └────┘└───────────────────────────┘   └─────────────┘
typ       └─────────┘  └─────┘  └────┘└───────────────────────────┘  └─────────────┘
doc       └─────────┘  └─────┘  └────┘                                └─────────────┘
txt       └─────────┘  └─────┘  └────┘                                └─────────────┘
par       └─────────┘  └─────┘  └────┘                                └─────────────┘
pid                         └┘                                                     
st     └────────────┘└───────┘└─────────────────────────────────────┘└───────────────┘└┘
658  
659  end limit
660  
661  
662  section colimit
663  
664  /-- `has_colimit F` represents a particular chosen colimit of the diagram `F`. -/
665  class has_colimit (F : J ⥤ C) :=
id                            
src                           
typ                           
doc                           
666  (cocone : cocone F)
id             └────┘ 
src            └────┘
typ            └────┘ 
doc            └────┘
667  (is_colimit : is_colimit cocone . tactic.apply_instance)
id                 └────────┘ └────┘ 
src                └────────┘
typ                └────────┘ └────┘ 
doc                └────────┘
668  
669  variables (J C)
670  
671  /-- `C` has colimits of shape `J` if we have chosen a particular colimit of
672    every functor `F : J ⥤ C`. -/
673  class has_colimits_of_shape :=
674  (has_colimit : Π F : J ⥤ C, has_colimit F)
id                           └─────────┘ 
src                             └─────────┘
typ                          └─────────┘ 
doc                             └─────────┘
675  
676  /-- `C` has all (small) colimits if it has colimits of every shape. -/
677  class has_colimits :=
678  (has_colimits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_colimits_of_shape J C)
id                                  └──┘         └────────────┘    └───────────────────┘  
src                                               └────────────┘     └───────────────────┘
typ                                 └──┘         └────────────┘    └───────────────────┘  
doc                                               └────────────┘     └───────────────────┘
679  
680  variables {J C}
681  
682  @[priority 100] -- see Note [lower instance priority]
683  instance has_colimit_of_has_colimits_of_shape
684    {J : Type v} [small_category J] [H : has_colimits_of_shape J C] (F : J ⥤ C) : has_colimit F :=
id                   └────────────┘        └───────────────────┘               └─────────┘ 
src                  └────────────┘         └───────────────────┘                   └─────────┘
typ                  └────────────┘        └───────────────────┘               └─────────┘ 
doc                  └────────────┘         └───────────────────┘                   └─────────┘
685  has_colimits_of_shape.has_colimit F
id   └───────────────────────────────┘ 
src  └───────────────────────────────┘
typ  └───────────────────────────────┘ 
686  
687  @[priority 100] -- see Note [lower instance priority]
688  instance has_colimits_of_shape_of_has_colimits
689    {J : Type v} [small_category J] [H : has_colimits.{v} C] : has_colimits_of_shape J C :=
id                   └────────────┘        └──────────┘         └───────────────────┘  
src                  └────────────┘         └──────────┘          └───────────────────┘
typ                  └────────────┘        └──────────┘         └───────────────────┘  
doc                  └────────────┘         └──────────┘          └───────────────────┘
690  has_colimits.has_colimits_of_shape C J
id   └────────────────────────────────┘  
src  └────────────────────────────────┘
typ  └────────────────────────────────┘  
691  
692  /- Interface to the `has_colimit` class. -/
693  
694  def colimit.cocone (F : J ⥤ C) [has_colimit F] : cocone F := has_colimit.cocone F
id                                └─────────┘     └────┘     └────────────────┘ 
src                                 └─────────┘      └────┘      └────────────────┘
typ                               └─────────┘     └────┘     └────────────────┘ 
doc                                 └─────────┘      └────┘
695  
696  def colimit (F : J ⥤ C) [has_colimit F] := (colimit.cocone F).X
id                         └─────────┘       └────────────┘  
src                          └─────────┘        └────────────┘   
typ                        └─────────┘       └────────────┘  
doc                          └─────────┘
697  
698  def colimit.ι (F : J ⥤ C) [has_colimit F] (j : J) : F.obj j ⟶ colimit F :=
id                           └─────────┘            └──┘   └─────┘ 
src                            └─────────┘               └──┘    └─────┘
typ                          └─────────┘            └──┘   └─────┘ 
doc                            └─────────┘
699  (colimit.cocone F).ι.app j
id    └────────────┘   └─┘  
src   └────────────┘    └─┘
typ   └────────────┘   └─┘  
700  
701  @[simp] lemma colimit.cocone_ι {F : J ⥤ C} [has_colimit F] (j : J) :
id                                            └─────────┘        
src                                             └─────────┘
typ                                           └─────────┘        
doc    └──┘                                     └─────────┘
702    (colimit.cocone F).ι.app j = colimit.ι _ j := rfl
id      └────────────┘   └─┘    └───────┘       └─┘
src     └────────────┘    └─┘     └───────┘        └─┘
typ     └────────────┘   └─┘    └───────┘       └─┘
703  
704  @[simp] lemma colimit.w (F : J ⥤ C) [has_colimit F] {j j' : J} (f : j ⟶ j') :
id                                     └─────────┘                    └┘
src                                      └─────────┘                      
typ                                    └─────────┘                    └┘
doc    └──┘                              └─────────┘
705    F.map f ≫ colimit.ι F j' = colimit.ι F j := (colimit.cocone F).w f
id     └──┘   └───────┘  └┘  └───────┘       └────────────┘    
src     └──┘    └───────┘       └───────┘         └────────────┘   
typ    └──┘   └───────┘  └┘  └───────┘       └────────────┘    
706  
707  def colimit.is_colimit (F : J ⥤ C) [has_colimit F] : is_colimit (colimit.cocone F) :=
id                                    └─────────┘     └────────┘  └────────────┘ 
src                                     └─────────┘      └────────┘  └────────────┘
typ                                   └─────────┘     └────────┘  └────────────┘ 
doc                                     └─────────┘      └────────┘
708  has_colimit.is_colimit.{v} F
id   └────────────────────┘     
src  └────────────────────┘
typ  └────────────────────┘     
709  
710  def colimit.desc (F : J ⥤ C) [has_colimit F] (c : cocone F) : colimit F ⟶ c.X :=
id                              └─────────┘        └────┘     └─────┘   └┘
src                               └─────────┘         └────┘      └─────┘     └┘
typ                             └─────────┘        └────┘     └─────┘   └┘
doc                               └─────────┘         └────┘
711  (colimit.is_colimit F).desc c
id    └────────────────┘  └──┘  
src   └────────────────┘   └──┘
typ   └────────────────┘  └──┘  
712  
713  @[simp] lemma colimit.is_colimit_desc {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id                                                   └─────────┘        └────┘ 
src                                                    └─────────┘         └────┘
typ                                                  └─────────┘        └────┘ 
doc    └──┘                                            └─────────┘         └────┘
714    (colimit.is_colimit F).desc c = colimit.desc F c := rfl
id      └────────────────┘  └──┘    └──────────┘      └─┘
src     └────────────────┘   └──┘     └──────────┘        └─┘
typ     └────────────────┘  └──┘    └──────────┘      └─┘
715  
716  /--
717  We have lots of lemmas describing how to simplify `colimit.ι F j ≫ _`,
718  and combined with `colimit.ext` we rely on these lemmas for many calculations.
719  
720  However, since `category.assoc` is a `@[simp]` lemma, often expressions are
721  right associated, and it's hard to apply these lemmas about `colimit.ι`.
722  
723  We thus use `reassoc` to define additional `@[simp]` lemmas, with an arbitrary extra morphism.
724  (see `tactic/reassoc_axiom.lean`)
725   -/
726  @[simp, reassoc] lemma colimit.ι_desc {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
id                                                   └─────────┘        └────┘        
src                                                    └─────────┘         └────┘
typ                                                  └─────────┘        └────┘        
doc    └──┘  └─────┘                                   └─────────┘         └────┘
727    colimit.ι F j ≫ colimit.desc F c = c.ι.app j :=
id     └───────┘    └──────────┘    └┘└──┘ 
src    └───────┘      └──────────┘       └┘└──┘
typ    └───────┘    └──────────┘    └┘└──┘ 
728  is_colimit.fac _ c j
id   └────────────┘    
typ  └────────────┘    
729  
730  def colimit.cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id                                         └─────────┘        └────┘ 
src                                          └─────────┘         └────┘
typ                                        └─────────┘        └────┘ 
doc                                          └─────────┘         └────┘
731    cocone_morphism (colimit.cocone F) c :=
id     └─────────────┘  └────────────┘   
src    └─────────────┘  └────────────┘
typ    └─────────────┘  └────────────┘   
732  (colimit.is_colimit F).desc_cocone_morphism c
id    └────────────────┘  └──────────────────┘  
src   └────────────────┘   └──────────────────┘
typ   └────────────────┘  └──────────────────┘  
733  
734  @[simp] lemma colimit.cocone_morphism_hom {F : J ⥤ C} [has_colimit F] (c : cocone F) :
id                                                       └─────────┘        └────┘ 
src                                                        └─────────┘         └────┘
typ                                                      └─────────┘        └────┘ 
doc    └──┘                                                └─────────┘         └────┘
735    (colimit.cocone_morphism c).hom = colimit.desc F c := rfl
id      └─────────────────────┘  └─┘   └──────────┘      └─┘
src     └─────────────────────┘   └─┘   └──────────┘        └─┘
typ     └─────────────────────┘  └─┘   └──────────┘      └─┘
736  @[simp] lemma colimit.ι_cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
id                                                     └─────────┘        └────┘        
src                                                      └─────────┘         └────┘
typ                                                    └─────────┘        └────┘        
doc    └──┘                                              └─────────┘         └────┘
737    colimit.ι F j ≫ (colimit.cocone_morphism c).hom = c.ι.app j :=
id     └───────┘     └─────────────────────┘  └─┘   └┘└──┘ 
src    └───────┘       └─────────────────────┘   └─┘    └┘└──┘
typ    └───────┘     └─────────────────────┘  └─┘   └┘└──┘ 
738  by erw is_colimit.fac
id          └────────────┘
src     └──┘              
typ     └──┘└────────────┘
doc     └──┘              
txt     └──┘              
par     └──┘              
pid                      
st     └───────────────────
739  
src  
typ  
doc  
txt  
par  
pid  
st   
740  @[ext] lemma colimit.hom_ext {F : J ⥤ C} [has_colimit F] {X : C} {f f' : colimit F ⟶ X}
id                                          └─────────┘                  └─────┘   
src                                           └─────────┘                    └─────┘   
typ                                         └─────────┘                  └─────┘   
doc    └─┘                                    └─────────┘
741    (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f' :=
id              └───────┘      └───────┘    └┘      └┘
src              └───────┘         └───────┘              
typ             └───────┘      └───────┘    └┘      └┘
742  (colimit.is_colimit F).hom_ext w
id    └────────────────┘  └─────┘  
src   └────────────────┘   └─────┘
typ   └────────────────┘  └─────┘  
doc                        └─────┘
743  
744  def colimit.hom_iso (F : J ⥤ C) [has_colimit F] (W : C) : (colimit F ⟶ W) ≅ (F.cocones.obj W) :=
id                                 └─────────┘             └─────┘       └──────┘└──┘ 
src                                  └─────────┘               └─────┘          └──────┘└──┘
typ                                └─────────┘             └─────┘       └──────┘└──┘ 
doc                                  └─────────┘                                  └──────┘
745  (colimit.is_colimit F).hom_iso W
id    └────────────────┘  └─────┘  
src   └────────────────┘   └─────┘
typ   └────────────────┘  └─────┘  
doc                        └─────┘
746  
747  @[simp] lemma colimit.hom_iso_hom (F : J ⥤ C) [has_colimit F] {W : C} (f : colimit F ⟶ W) :
id                                               └─────────┘               └─────┘   
src                                                └─────────┘                 └─────┘   
typ                                              └─────────┘               └─────┘   
doc    └──┘                                        └─────────┘
748    (colimit.hom_iso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f :=
id      └─────────────┘   └─┘     └────────────┘      └───┘  └─┘  
src     └─────────────┘     └─┘      └────────────┘       └───┘   └─┘
typ     └─────────────┘   └─┘     └────────────┘      └───┘  └─┘  
749  (colimit.is_colimit F).hom_iso_hom f
id    └────────────────┘  └─────────┘  
src   └────────────────┘   └─────────┘
typ   └────────────────┘  └─────────┘  
750  
751  def colimit.hom_iso' (F : J ⥤ C) [has_colimit F] (W : C) :
id                                  └─────────┘        
src                                   └─────────┘
typ                                 └─────────┘        
doc                                   └─────────┘
752    ((colimit F ⟶ W) : Type v) ≅ { p : Π j, F.obj j ⟶ W // ∀ {j j'} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
id       └─────┘                         └──┘           └┘         └┘   └──┘    └┘   
src      └─────┘                             └──┘                                └──┘         
typ      └─────┘                         └──┘           └┘         └┘   └──┘    └┘   
753  (colimit.is_colimit F).hom_iso' W
id    └────────────────┘  └──────┘  
src   └────────────────┘   └──────┘
typ   └────────────────┘  └──────┘  
754  
755  lemma colimit.desc_extend (F : J ⥤ C) [has_colimit F] (c : cocone F) {X : C} (f : c.X ⟶ X) :
id                                       └─────────┘        └────┘               └┘  
src                                        └─────────┘         └────┘                  └┘ 
typ                                      └─────────┘        └────┘               └┘  
doc                                        └─────────┘         └────┘
756    colimit.desc F (c.extend f) = colimit.desc F c ≫ f :=
id     └──────────┘   └─────┘    └──────────┘    
src    └──────────┘     └─────┘     └──────────┘     
typ    └──────────┘   └─────┘    └──────────┘    
doc                     └─────┘
757  begin
st   └─────
758    ext1, rw [←category.assoc], simp
id                └────────────┘
src    └──┘  └───┘└────────────┘  └───┘
typ    └──┘  └───┘└────────────┘  └───┘
doc    └──┘  └───┘                └───┘
txt    └──┘  └───┘                └───┘
par    └──┘  └───┘                └───┘
pid            └─┘                    
st   ─────┘└───────────────────┘└──────┘
759  end
st   └─┘
760  
761  def has_colimit_of_iso {F G : J ⥤ C} [has_colimit F] (α : G ≅ F) : has_colimit G :=
id                                      └─────────┘              └─────────┘ 
src                                       └─────────┘                 └─────────┘
typ                                     └─────────┘              └─────────┘ 
doc                                       └─────────┘                  └─────────┘
762  { cocone := (cocones.precompose α.hom).obj (colimit.cocone F),
id                └────────────────┘ └──┘ └─┘   └────────────┘ 
src               └────────────────┘  └──┘ └─┘   └────────────┘
typ               └────────────────┘ └──┘ └─┘   └────────────┘ 
763    is_colimit :=
764    { desc := λ s, colimit.desc F ((cocones.precompose α.inv).obj s),
id                   └──────────┘    └────────────────┘ └──┘ └─┘  
src                   └──────────┘     └────────────────┘  └──┘ └─┘
typ                  └──────────┘    └────────────────┘ └──┘ └─┘  
765      fac' := λ s j,
id                  
typ                 
766      begin
st       └─────
767        rw [cocones.precompose_obj_ι, nat_trans.comp_app, colimit.cocone_ι],
id             └──────────────────────┘  └────────────────┘  └──────────────┘
src        └──┘└──────────────────────┘└┘└────────────────┘└┘└──────────────┘
typ        └──┘└──────────────────────┘└┘└────────────────┘└┘└──────────────┘
doc        └──┘                        └┘                  └┘                
txt        └──┘                        └┘                  └┘                
par        └──┘                        └┘                  └┘                
pid          └┘                        └┘                  └┘                
st   ─────────────────────────────────┘└──────────────────┘└────────────────┘└──
768        rw [category.assoc, colimit.ι_desc, ←nat_iso.app_hom, ←iso.eq_inv_comp], refl
id             └────────────┘  └────────────┘   └─────────────┘   └─────────────┘
src        └──┘└────────────┘└┘└────────────┘└─┘└─────────────┘└─┘└─────────────┘  └────
typ        └──┘└────────────┘└┘└────────────┘└─┘└─────────────┘└─┘└─────────────┘  └────
doc        └──┘              └┘└────────────┘└─┘               └─┘                 └────
txt        └──┘              └┘              └─┘               └─┘                 └────
par        └──┘              └┘              └─┘               └─┘                 └────
pid          └┘              └┘              └─┘               └─┘                     
st   ───────────────────────┘└──────────────┘└────────────────┘└────────────────┘└───────
769      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
770      uniq' := λ s m w,
id                    
typ                   
771      begin
st       └─────
772        apply colimit.hom_ext, intro j,
id               └─────────────┘
src        └────┘└─────────────┘  └─────┘
typ        └────┘└─────────────┘  └─────┘
doc        └────┘                 └─────┘
txt        └────┘                 └─────┘
par        └────┘                 └─────┘
pid                                   └┘
st   ──────────────────────────┘└───────┘└─
773        rw [colimit.ι_desc, cocones.precompose_obj_ι, nat_trans.comp_app, ←nat_iso.app_inv,
id             └────────────┘  └──────────────────────┘  └────────────────┘   └─────────────┘
src        └──┘└────────────┘└┘└──────────────────────┘└┘└────────────────┘└─┘└─────────────┘└─
typ        └──┘└────────────┘└┘└──────────────────────┘└┘└────────────────┘└─┘└─────────────┘└─
doc        └──┘└────────────┘└┘                        └┘                  └─┘               └─
txt        └──┘              └┘                        └┘                  └─┘               └─
par        └──┘              └┘                        └┘                  └─┘               └─
pid          └┘              └┘                        └┘                  └─┘               └─
st   ───────────────────────┘└────────────────────────┘└──────────────────┘└────────────────┘└─
774          iso.eq_inv_comp],
id           └─────────────┘
src  ───────┘└─────────────┘
typ  ───────┘└─────────────┘
doc  ───────┘               
txt  ───────┘               
par  ───────┘               
pid  ───────┘               
st   ──────────────────────┘└──
775        simpa using w j
id                      
src        └──────────┘  
typ        └──────────┘
doc        └──────────┘  
txt        └──────────┘  
par        └──────────┘  
pid             └────┘  
st   ──────────────────────
776      end } }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
777  
778  /-- If a functor `G` has the same collection of cocones as a functor `F`
779  which has a colimit, then `G` also has a colimit. -/
780  def has_colimit.of_cocones_iso {J K : Type v} [small_category J] [small_category K] (F : J ⥤ C) (G : K ⥤ C)
id                                                  └────────────┘    └────────────┘                   
src                                                 └────────────┘     └────────────┘                      
typ                                                 └────────────┘    └────────────┘                   
doc                                                 └────────────┘     └────────────┘                      
781    (h : F.cocones ≅ G.cocones) [has_colimit F] : has_colimit G :=
id          └──────┘  └──────┘   └─────────┘     └─────────┘ 
src          └──────┘   └──────┘   └─────────┘      └─────────┘
typ         └──────┘  └──────┘   └─────────┘     └─────────┘ 
doc          └──────┘    └──────┘   └─────────┘      └─────────┘
782  ⟨_, is_colimit.of_nat_iso ((is_colimit.nat_iso (colimit.is_colimit F)) ≪≫ h)⟩
id       └───────────────────┘   └────────────────┘  └────────────────┘    └┘ 
src      └───────────────────┘   └────────────────┘  └────────────────┘     └┘
typ      └───────────────────┘   └────────────────┘  └────────────────┘    └┘ 
doc      └───────────────────┘   └────────────────┘
783  
784  section pre
785  variables (F) [has_colimit F] (E : K ⥤ J) [has_colimit (E ⋙ F)]
id                  └─────────┘                └─────────┘    
src                 └─────────┘                └─────────┘    
typ                 └─────────┘                └─────────┘    
doc                 └─────────┘                └─────────┘    
786  
787  def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
id                     └─────┘       └─────┘ 
src                    └─────┘         └─────┘
typ                    └─────┘       └─────┘ 
doc                               
788  colimit.desc (E ⋙ F)
id   └──────────┘    
src  └──────────┘    
typ  └──────────┘    
doc                  
789    { X := colimit F,
id            └─────┘ 
src           └─────┘
typ           └─────┘ 
790      ι := { app := λ k, colimit.ι F (E.obj k) } }
id                        └───────┘   └──┘ 
src                        └───────┘     └──┘
typ                       └───────┘   └──┘ 
doc           
791  
792  @[simp, reassoc] lemma colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
id                                                 └───────┘        └─────────┘    └───────┘   └──┘ 
src                                                 └───────┘           └─────────┘      └───────┘     └──┘
typ                                                └───────┘        └─────────┘    └───────┘   └──┘ 
doc    └──┘  └─────┘                                             
793  by erw is_colimit.fac
id          └────────────┘
src     └──┘              
typ     └──┘└────────────┘
doc     └──┘              
txt     └──┘              
par     └──┘              
pid                      
st     └───────────────────
794  
src  
typ  
doc  
txt  
par  
pid  
st   
795  @[simp] lemma colimit.pre_desc (c : cocone F) :
id                                       └────┘ 
src                                      └────┘
typ                                      └────┘ 
doc    └──┘                              └────┘
796    colimit.pre F E ≫ colimit.desc F c = colimit.desc (E ⋙ F) (c.whisker E) :=
id     └─────────┘    └──────────┘    └──────────┘       └──────┘ 
src    └─────────┘      └──────────┘      └──────────┘          └──────┘
typ    └─────────┘    └──────────┘    └──────────┘       └──────┘ 
doc                                                         
797  by ext; rw [←assoc, colimit.ι_pre]; simp
id                └───┘  └───────────┘
src     └─┘  └───┘└───┘└┘└───────────┘  └────
typ     └─┘  └───┘└───┘└┘└───────────┘  └────
doc     └─┘  └───┘     └┘               └────
txt     └─┘  └───┘     └┘               └────
par     └─┘  └───┘     └┘               └────
pid            └─┘     └┘                   
st     └────────┘└────┘└─────────────┘└──────
798  
src  
typ  
doc  
txt  
par  
pid  
st   
799  variables {L : Type v} [small_category L]
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
doc                          └────────────┘
800  variables (D : L ⥤ K) [has_colimit (D ⋙ E ⋙ F)]
id                         └─────────┘       
src                        └─────────┘       
typ                        └─────────┘       
doc                        └─────────┘       
801  
802  @[simp] lemma colimit.pre_pre : colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) :=
id                                   └─────────┘        └─────────┘    └─────────┘     
src                                  └─────────┘           └─────────┘      └─────────┘      
typ                                  └─────────┘        └─────────┘    └─────────┘     
doc    └──┘                                                                                    
803  begin
st   └─────
804    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
805    rw [←assoc, colimit.ι_pre, colimit.ι_pre],
id          └───┘  └───────────┘  └───────────┘
src    └───┘└───┘└┘└───────────┘└┘└───────────┘
typ    └───┘└───┘└┘└───────────┘└┘└───────────┘
doc    └───┘     └┘             └┘             
txt    └───┘     └┘             └┘             
par    └───┘     └┘             └┘             
pid      └─┘     └┘             └┘             
st   ───────────┘└─────────────┘└─────────────┘└──
806    letI : has_colimit ((D ⋙ E) ⋙ F) := show has_colimit (D ⋙ E ⋙ F), by apply_instance,
id            └─────────┘                   └─────────┘        
src    └─────┘└─────────┘    └┘  └───┘    └─────────┘      └────┘└────────────┘
typ    └─────┘└─────────┘  └┘ └───┘    └─────────┘   └────┘└────────────┘
doc    └─────┘└─────────┘    └┘  └───┘    └─────────┘      └────┘└────────────┘
txt    └─────┘                └┘  └───┘                     └────┘└────────────┘
par    └─────┘                └┘  └───┘                     └────┘└────────────┘
pid        └┘                └┘  └──┘                     └──────────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─────────────┘└─
807    exact (colimit.ι_pre F (D ⋙ E) j).symm
id            └───────────┘        
src    └────┘ └───────────┘     └┘ └─────┘
typ    └────┘ └───────────┘  └┘└─────┘
doc    └────┘                   └┘ └─────┘
txt    └────┘                   └┘ └─────┘
par    └────┘                   └┘ └─────┘
pid                            └┘ └───┘└┘
st   ────────────────────────────────────────┘
808  end
st   └─┘
809  
810  end pre
811  
812  section post
813  variables {D : Type u'} [𝒟 : category.{v} D]
id                                └──────┘
src                               └──────┘
typ                               └──────┘
doc                               └──────┘
814  include 𝒟
815  
816  variables (F) [has_colimit F] (G : C ⥤ D) [has_colimit (F ⋙ G)]
id                  └─────────┘                └─────────┘    
src                 └─────────┘                └─────────┘    
typ                 └─────────┘                └─────────┘    
doc                 └─────────┘                └─────────┘    
817  
818  def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
id                      └─────┘       └──┘  └─────┘ 
src                     └─────┘          └──┘  └─────┘
typ                     └─────┘       └──┘  └─────┘ 
doc                                
819  colimit.desc (F ⋙ G)
id   └──────────┘    
src  └──────────┘    
typ  └──────────┘    
doc                  
820  { X := G.obj (colimit F),
id          └──┘  └─────┘ 
src          └──┘  └─────┘
typ         └──┘  └─────┘ 
821    ι :=
822    { app := λ j, G.map (colimit.ι F j),
id                  └──┘  └───────┘  
src                   └──┘  └───────┘
typ                 └──┘  └───────┘  
823      naturality' :=
824        by intros j j' f; erw [←G.map_comp, limits.cocone.w, comp_id]; refl } }
id                                             └─────────────┘  └─────┘
src           └───────────┘  └────┘          └┘└─────────────┘└┘└─────┘  └───┘
typ           └───────────┘  └────┘└────────┘└┘└─────────────┘└┘└─────┘  └───┘
doc           └───────────┘  └────┘          └┘               └┘         └───┘
txt           └───────────┘  └────┘          └┘               └┘         └───┘
par           └───────────┘  └────┘          └┘               └┘         └───┘
pid                 └─────┘     └─┘          └┘               └┘             
st           └───────────────────┘└─────────┘└───────────────┘└───────┘└─────┘
825  
826  @[simp, reassoc] lemma colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G  = G.map (colimit.ι F j) :=
id                                                  └───────┘        └──────────┘     └──┘  └───────┘  
src                                                  └───────┘           └──────────┘        └──┘  └───────┘
typ                                                 └───────┘        └──────────┘     └──┘  └───────┘  
doc    └──┘  └─────┘                                              
827  by erw is_colimit.fac
id          └────────────┘
src     └──┘              
typ     └──┘└────────────┘
doc     └──┘              
txt     └──┘              
par     └──┘              
pid                      
st     └───────────────────
828  
src  
typ  
doc  
txt  
par  
pid  
st   
829  @[simp] lemma colimit.post_desc (c : cocone F) :
id                                        └────┘ 
src                                       └────┘
typ                                       └────┘ 
doc    └──┘                               └────┘
830    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.map_cocone c) :=
id     └──────────┘    └──┘  └──────────┘     └──────────┘       └─────────┘ 
src    └──────────┘       └──┘  └──────────┘       └──────────┘          └─────────┘
typ    └──────────┘    └──┘  └──────────┘     └──────────┘       └─────────┘ 
doc                                                                        └─────────┘
831  by ext; rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_desc, colimit.ι_desc]; refl
id                └───┘  └────────────┘               └────────────┘  └────────────┘
src     └─┘  └───┘└───┘└┘└────────────┘└─┘          └┘└────────────┘└┘└────────────┘  └────
typ     └─┘  └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└────────────┘└┘└────────────┘  └────
doc     └─┘  └───┘     └┘              └─┘          └┘└────────────┘└┘└────────────┘  └────
txt     └─┘  └───┘     └┘              └─┘          └┘              └┘                └────
par     └─┘  └───┘     └┘              └─┘          └┘              └┘                └────
pid            └─┘     └┘              └─┘          └┘              └┘                    
st     └────────┘└────┘└──────────────┘└───────────┘└──────────────┘└──────────────┘└──────
832  
src  
typ  
doc  
txt  
par  
pid  
st   
833  @[simp] lemma colimit.post_post
doc    └──┘
834    {E : Type u''} [category.{v} E] (H : D ⥤ E) [has_colimit ((F ⋙ G) ⋙ H)] :
id                     └──────┘                 └─────────┘        
src                    └──────┘                    └─────────┘         
typ                    └──────┘                 └─────────┘        
doc                    └──────┘                    └─────────┘         
835  /- H G (colimit F) ⟶ H (colimit (F ⋙ G)) ⟶ colimit ((F ⋙ G) ⋙ H) equals -/
836  /- H G (colimit F) ⟶ colimit (F ⋙ (G ⋙ H)) -/
837    colimit.post (F ⋙ G) H ≫ H.map (colimit.post F G) = colimit.post F (G ⋙ H) :=
id     └──────────┘        └──┘  └──────────┘     └──────────┘     
src    └──────────┘            └──┘  └──────────┘       └──────────┘      
typ    └──────────┘        └──┘  └──────────┘     └──────────┘     
doc                                                                         
838  begin
st   └─────
839    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
840    rw [←assoc, colimit.ι_post, ←H.map_comp, colimit.ι_post],
id          └───┘  └────────────┘               └────────────┘
src    └───┘└───┘└┘└────────────┘└─┘          └┘└────────────┘
typ    └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└────────────┘
doc    └───┘     └┘              └─┘          └┘              
txt    └───┘     └┘              └─┘          └┘              
par    └───┘     └┘              └─┘          └┘              
pid      └─┘     └┘              └─┘          └┘              
st   ───────────┘└──────────────┘└───────────┘└──────────────┘└──
841    exact (colimit.ι_post F (G ⋙ H) j).symm
id            └────────────┘       
src    └────┘ └────────────┘    └┘ └─────┘
typ    └────┘ └────────────┘ └┘└─────┘
doc    └────┘                   └┘ └─────┘
txt    └────┘                    └┘ └─────┘
par    └────┘                    └┘ └─────┘
pid                             └┘ └───┘└┘
st   ─────────────────────────────────────────┘
842  end
st   └─┘
843  
844  end post
845  
846  lemma colimit.pre_post {D : Type u'} [category.{v} D]
id                                         └──────┘     
src                                        └──────┘
typ                                        └──────┘     
doc                                        └──────┘
847    (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
id                              
src                                 
typ                             
doc                                 
848    [has_colimit F] [has_colimit (E ⋙ F)] [has_colimit (F ⋙ G)] [has_colimit ((E ⋙ F) ⋙ G)] :
id      └─────────┘    └─────────┘        └─────────┘        └─────────┘        
src     └─────────┘     └─────────┘          └─────────┘          └─────────┘         
typ     └─────────┘    └─────────┘        └─────────┘        └─────────┘        
doc     └─────────┘     └─────────┘          └─────────┘          └─────────┘         
849  /- G (colimit F) ⟶ G (colimit (E ⋙ F)) ⟶ colimit ((E ⋙ F) ⋙ G) vs -/
850  /- G (colimit F) ⟶ colimit F ⋙ G ⟶ colimit (E ⋙ (F ⋙ G)) or -/
851    colimit.post (E ⋙ F) G ≫ G.map (colimit.pre F E) = colimit.pre (F ⋙ G) E ≫ colimit.post F G :=
id     └──────────┘        └──┘  └─────────┘     └─────────┘        └──────────┘  
src    └──────────┘            └──┘  └─────────┘       └─────────┘           └──────────┘
typ    └──────────┘        └──┘  └─────────┘     └─────────┘        └──────────┘  
doc                                                                     
852  begin
st   └─────
853    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
854    rw [←assoc, colimit.ι_post, ←G.map_comp, colimit.ι_pre, ←assoc],
id          └───┘  └────────────┘               └───────────┘   └───┘
src    └───┘└───┘└┘└────────────┘└─┘          └┘└───────────┘└─┘└───┘
typ    └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└───────────┘└─┘└───┘
doc    └───┘     └┘              └─┘          └┘             └─┘     
txt    └───┘     └┘              └─┘          └┘             └─┘     
par    └───┘     └┘              └─┘          └┘             └─┘     
pid      └─┘     └┘              └─┘          └┘             └─┘     
st   ───────────┘└──────────────┘└───────────┘└─────────────┘└──────┘└──
855    letI : has_colimit (E ⋙ F ⋙ G) := show has_colimit ((E ⋙ F) ⋙ G), by apply_instance,
id            └─────────┘                 └─────────┘          
src    └─────┘└─────────┘     └───┘    └─────────┘     └┘  └────┘└────────────┘
typ    └─────┘└─────────┘  └───┘    └─────────┘   └┘ └────┘└────────────┘
doc    └─────┘└─────────┘     └───┘    └─────────┘     └┘  └────┘└────────────┘
txt    └─────┘                 └───┘                    └┘  └────┘└────────────┘
par    └─────┘                 └───┘                    └┘  └────┘└────────────┘
pid        └┘                 └──┘                    └┘  └──────────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─────────────┘└─
856    erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
id          └───────────┘          └────────────┘
src    └───┘└───────────┘    └┘  └┘└────────────┘└┘
typ    └───┘└───────────┘  └┘└┘└────────────┘└┘
doc    └───┘                 └┘  └┘              └┘
txt    └───┘                 └┘  └┘              └┘
par    └───┘                 └┘  └┘              └┘
pid       └┘                 └┘  └┘              
st   ───────────────────────────────┘└──────────────┘
857  end
st   └─┘
858  
859  open category_theory.equivalence
860  instance has_colimit_equivalence_comp (e : K ≌ J) [has_colimit F] : has_colimit (e.functor ⋙ F) :=
id                                                   └─────────┘     └─────────┘  └──────┘  
src                                                    └─────────┘      └─────────┘   └──────┘ 
typ                                                  └─────────┘     └─────────┘  └──────┘  
doc                                                    └─────────┘      └─────────┘            
861  { cocone := cocone.whisker e.functor (colimit.cocone F),
id               └────────────┘ └──────┘  └────────────┘ 
src              └────────────┘  └──────┘  └────────────┘
typ              └────────────┘ └──────┘  └────────────┘ 
862    is_colimit := let e' := cocones.precompose (e.inv_fun_id_assoc F).inv in
id                       └┘    └────────────────┘  └───────────────┘  └─┘
src                            └────────────────┘   └───────────────┘   └─┘
typ                      └┘    └────────────────┘  └───────────────┘  └─┘
863    { desc := λ s, colimit.desc F (e'.obj (cocone.whisker e.inverse s)),
id                   └──────────┘   └┘└──┘  └────────────┘ └──────┘ 
src                   └──────────┘      └──┘  └────────────┘  └──────┘
typ                  └──────────┘   └┘└──┘  └────────────┘ └──────┘ 
864      fac' := λ s j,
id                  
typ                 
865      begin
st       └─────
866        dsimp, rw [colimit.ι_desc], dsimp [e'],
id                    └────────────┘          └┘
src        └───┘  └──┘└────────────┘  └─────┘  
typ        └───┘  └──┘└────────────┘  └─────┘└┘
doc        └───┘  └──┘└────────────┘  └─────┘  
txt        └───┘  └──┘                └─────┘  
par        └───┘  └──┘                └─────┘  
pid                 └┘                       
st   ──────────┘└──────────────────┘└───────────┘└─
867        erw [inv_fun_id_assoc_inv_app, ←functor_unit, s.ι.naturality, comp_id], refl
id              └──────────────────────┘   └──────────┘                  └─────┘
src        └───┘└──────────────────────┘└─┘└──────────┘└┘              └┘└─────┘  └────
typ        └───┘└──────────────────────┘└─┘└──────────┘└┘└────────────┘└┘└─────┘  └────
doc        └───┘                        └─┘            └┘              └┘         └────
txt        └───┘                        └─┘            └┘              └┘         └────
par        └───┘                        └─┘            └┘              └┘         └────
pid           └┘                        └─┘            └┘              └┘             
st   ──────────────────────────────────┘└─────────────┘└──────────────┘└───────┘└───────
868      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
869      uniq' := λ s m w,
id                    
typ                   
870      begin
st       └─────
871        apply colimit.hom_ext, intro j,
id               └─────────────┘
src        └────┘└─────────────┘  └─────┘
typ        └────┘└─────────────┘  └─────┘
doc        └────┘                 └─────┘
txt        └────┘                 └─────┘
par        └────┘                 └─────┘
pid                                   └┘
st   ──────────────────────────┘└───────┘└─
872        erw [colimit.ι_desc],
id              └────────────┘
src        └───┘└────────────┘
typ        └───┘└────────────┘
doc        └───┘└────────────┘
txt        └───┘              
par        └───┘              
pid           └┘              
st   ────────────────────────┘└──
873        have := w (e.inverse.obj j), simp at this, erw [←colimit.w F (e.counit_iso.hom.app j)] at this,
id                   └───────────┘                        └───────┘   └──────────────────┘ 
src        └──────┘  └───────────┘   └──────────┘  └────┘└───────┘  └──────────────────┘ └────────┘
typ        └──────┘ └───────────┘  └──────────┘  └────┘└───────┘ └──────────────────┘└────────┘
doc        └──────┘                  └──────────┘  └────┘                                └────────┘
txt        └──────┘                  └──────────┘  └────┘                                └────────┘
par        └──────┘                  └──────────┘  └────┘                                └────────┘
pid        └───┘└─┘                      └─────┘     └─┘                                └┘└──────┘
st   ────────────────────────────────┘└────────────┘└──────────────────────────────────────────┘└──────┘└─
874        erw [assoc, ←iso.eq_inv_comp (F.map_iso $ e.counit_iso.app j)] at this, erw [this], simp
id              └───┘   └─────────────┘  └───────┘   └──────────────┘                  └──┘
src        └───┘└───┘└─┘└─────────────┘ └───────┘ └──────────────┘ └────────┘  └───┘      └────
typ        └───┘└───┘└─┘└─────────────┘ └───────┘ └──────────────┘└────────┘  └───┘└──┘  └────
doc        └───┘     └─┘                          └──────────────┘ └────────┘  └───┘      └────
txt        └───┘     └─┘                                           └────────┘  └───┘      └────
par        └───┘     └─┘                                           └────────┘  └───┘      └────
pid           └┘     └─┘                                           └┘└──────┘     └┘          
st   ───────────────┘└─────────────────────────────────────────────────┘└──────┘└─────────┘└───────
875      end } }
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
876  
877  def has_colimit_of_equivalence_comp (e : K ≌ J) [has_colimit (e.functor ⋙ F)] : has_colimit F :=
id                                                 └─────────┘  └──────┘       └─────────┘ 
src                                                  └─────────┘   └──────┘        └─────────┘
typ                                                └─────────┘  └──────┘       └─────────┘ 
doc                                                  └─────────┘                   └─────────┘
878  begin
st   └─────
879    haveI : has_colimit (e.inverse ⋙ e.functor ⋙ F) := limits.has_colimit_equivalence_comp e.symm,
id             └─────────┘  └───────┘  └───────┘        └─────────────────────────────────┘ └────┘
src    └──────┘└─────────┘ └───────┘└───────┘  └───┘└─────────────────────────────────┘└────┘
typ    └──────┘└─────────┘ └───────┘└───────┘ └───┘└─────────────────────────────────┘└────┘
doc    └──────┘└─────────┘                     └───┘                                   
txt    └──────┘                                 └───┘                                   
par    └──────┘                                 └───┘                                   
pid         └┘                                 └──┘                                   
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
880    apply has_colimit_of_iso (e.inv_fun_id_assoc F).symm,
id           └────────────────┘  └────────────────┘ 
src    └────┘└────────────────┘ └────────────────┘ └────┘
typ    └────┘└────────────────┘ └────────────────┘└────┘
doc    └────┘                                      └────┘
txt    └────┘                                      └────┘
par    └────┘                                      └────┘
pid                                               └───┘
st   ─────────────────────────────────────────────────────┘└─
881  end
st   ──┘
882  
883  section colim_functor
884  
885  variables [has_colimits_of_shape J C]
id              └───────────────────┘
src             └───────────────────┘
typ             └───────────────────┘
doc             └───────────────────┘
886  
887  /-- `colimit F` is functorial in `F`, when `C` has all colimits of shape `J`. -/
888  def colim : (J ⥤ C) ⥤ C :=
id                     
src                     
typ                    
doc                     
889  { obj := λ F, colimit F,
id               └─────┘ 
src               └─────┘
typ              └─────┘ 
doc  
890    map := λ F G α, colimit.desc F
id                  └──────────┘ 
src                    └──────────┘
typ                 └──────────┘ 
891      { X := colimit G,
id              └─────┘ 
src             └─────┘
typ             └─────┘ 
892        ι :=
893        { app := λ j, α.app j ≫ colimit.ι G j,
id                      └──┘   └───────┘  
src                       └──┘    └───────┘
typ                     └──┘   └───────┘  
894          naturality' := λ j j' f,
id                             └┘ 
typ                            └┘ 
895            by erw [comp_id, ←assoc, α.naturality, assoc, colimit.w] } },
id                     └─────┘   └───┘                └───┘  └───────┘
src               └───┘└─────┘└─┘└───┘└┘            └┘└───┘└┘└───────┘└┘
typ               └───┘└─────┘└─┘└───┘└┘└──────────┘└┘└───┘└┘└───────┘└┘
doc               └───┘       └─┘     └┘            └┘     └┘         └┘
txt               └───┘       └─┘     └┘            └┘     └┘         └┘
par               └───┘       └─┘     └┘            └┘     └┘         └┘
pid                  └┘       └─┘     └┘            └┘     └┘         
st               └───────────┘└──────┘└────────────┘└─────┘└─────────┘
896    map_comp' := λ F G H α β,
id                        
typ                       
897      by ext; erw [←assoc, is_colimit.fac, is_colimit.fac, assoc, is_colimit.fac, ←assoc]; refl }
id                     └───┘  └────────────┘  └────────────┘  └───┘  └────────────┘   └───┘
src         └─┘  └────┘└───┘└┘              └┘              └┘└───┘└┘              └─┘└───┘  └───┘
typ         └─┘  └────┘└───┘└┘└────────────┘└┘└────────────┘└┘└───┘└┘└────────────┘└─┘└───┘  └───┘
doc         └─┘  └────┘     └┘              └┘              └┘     └┘              └─┘       └───┘
txt         └─┘  └────┘     └┘              └┘              └┘     └┘              └─┘       └───┘
par         └─┘  └────┘     └┘              └┘              └┘     └┘              └─┘       └───┘
pid                 └─┘     └┘              └┘              └┘     └┘              └─┘           
st         └─────────┘└────────────────────────────────────────────────────────────────────┘└─────┘
898  
899  variables {F} {G : J ⥤ C} (α : F ⟶ G)
id                                   
src                                  
typ                                  
doc                       
900  
901  @[simp, reassoc] lemma colim.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j :=
id                                               └───────┘    └───┘└──┘   └──┘   └───────┘  
src                                               └───────┘      └───┘└──┘     └──┘    └───────┘
typ                                              └───────┘    └───┘└──┘   └──┘   └───────┘  
doc    └──┘  └─────┘                                              └───┘
902  by apply is_colimit.fac
id            └────────────┘
src     └────┘              
typ     └────┘└────────────┘
doc     └────┘              
txt     └────┘              
par     └────┘              
pid                        
st     └─────────────────────
903  
src  
typ  
doc  
txt  
par  
pid  
st   
904  @[simp] lemma colimit.map_desc (c : cocone G) :
id                                       └────┘ 
src                                      └────┘
typ                                      └────┘ 
doc    └──┘                              └────┘
905    colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
id     └───┘└──┘   └──────────┘    └──────────┘    └────────────────┘  └─┘  
src    └───┘└──┘    └──────────┘      └──────────┘     └────────────────┘   └─┘
typ    └───┘└──┘   └──────────┘    └──────────┘    └────────────────┘  └─┘  
doc    └───┘
906  by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
id                └───┘  └─────────┘  └───┘  └────────────┘  └────────────┘
src     └─┘  └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘└┘└────────────┘  └────
typ     └─┘  └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘└┘└────────────┘  └────
doc     └─┘  └───┘     └┘           └┘     └┘└────────────┘└┘└────────────┘  └────
txt     └─┘  └───┘     └┘           └┘     └┘              └┘                └────
par     └─┘  └───┘     └┘           └┘     └┘              └┘                └────
pid            └─┘     └┘           └┘     └┘              └┘                    
st     └────────┘└────┘└───────────┘└─────┘└──────────────┘└──────────────┘└──────
907  
src  
typ  
doc  
txt  
par  
pid  
st   
908  lemma colimit.pre_map [has_colimits_of_shape K C] (E : K ⥤ J) :
id                          └───────────────────┘           
src                         └───────────────────┘             
typ                         └───────────────────┘           
doc                         └───────────────────┘             
909    colimit.pre F E ≫ colim.map α = colim.map (whisker_left E α) ≫ colimit.pre G E :=
id     └─────────┘    └───┘└──┘   └───┘└──┘  └──────────┘     └─────────┘  
src    └─────────┘      └───┘└──┘    └───┘└──┘  └──────────┘       └─────────┘
typ    └─────────┘    └───┘└──┘   └───┘└──┘  └──────────┘     └─────────┘  
doc                      └───┘         └───┘
910  by ext; rw [←assoc, colimit.ι_pre, colim.ι_map, ←assoc, colim.ι_map, assoc, colimit.ι_pre]; refl
id                └───┘  └───────────┘  └─────────┘   └───┘  └─────────┘  └───┘  └───────────┘
src     └─┘  └───┘└───┘└┘└───────────┘└┘└─────────┘└─┘└───┘└┘└─────────┘└┘└───┘└┘└───────────┘  └────
typ     └─┘  └───┘└───┘└┘└───────────┘└┘└─────────┘└─┘└───┘└┘└─────────┘└┘└───┘└┘└───────────┘  └────
doc     └─┘  └───┘     └┘             └┘           └─┘     └┘           └┘     └┘               └────
txt     └─┘  └───┘     └┘             └┘           └─┘     └┘           └┘     └┘               └────
par     └─┘  └───┘     └┘             └┘           └─┘     └┘           └┘     └┘               └────
pid            └─┘     └┘             └┘           └─┘     └┘           └┘     └┘                   
st     └────────┘└────┘└─────────────┘└───────────┘└──────┘└───────────┘└─────┘└─────────────┘└──────
911  
src  
typ  
doc  
txt  
par  
pid  
st   
912  lemma colimit.pre_map' [has_colimits_of_shape.{v} K C]
id                           └───────────────────┘      
src                          └───────────────────┘
typ                          └───────────────────┘      
doc                          └───────────────────┘
913    (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
id                                └┘  └┘
src                                      
typ                               └┘  └┘
doc                          
914    colimit.pre F E₁ = colim.map (whisker_right α F) ≫ colimit.pre F E₂ :=
id     └─────────┘  └┘  └───┘└──┘  └───────────┘     └─────────┘  └┘
src    └─────────┘       └───┘└──┘  └───────────┘       └─────────┘
typ    └─────────┘  └┘  └───┘└──┘  └───────────┘     └─────────┘  └┘
doc                       └───┘
915  by ext1; simp [(category.assoc _ _ _ _).symm]
id                   └────────────┘
src     └──┘  └────┘ └────────────┘└───────────────
typ     └──┘  └────┘ └────────────┘└───────────────
doc     └──┘  └────┘               └───────────────
txt     └──┘  └────┘               └───────────────
par     └──┘  └────┘               └───────────────
pid                              └─────────────┘
st     └───────────────────────────────────────────
916  
src  
typ  
doc  
txt  
par  
pid  
st   
917  lemma colimit.pre_id (F : J ⥤ C) :
id                               
src                              
typ                              
doc                              
918  colimit.pre F (𝟭 _) = colim.map (functor.left_unitor F).hom := by tidy
id   └─────────┘        └───┘└──┘  └─────────────────┘  └─┘
src  └─────────┘         └───┘└──┘  └─────────────────┘   └─┘        └────
typ  └─────────┘        └───┘└──┘  └─────────────────┘  └─┘        └────
doc                       └───┘                                       └────
txt                                                                    └────
par                                                                    └────
pid                                                                        
st                                                                    └─────
919  
src  
typ  
doc  
txt  
par  
pid  
st   
920  lemma colimit.map_post {D : Type u'} [category.{v} D] [has_colimits_of_shape J D] (H : C ⥤ D) :
id                                         └──────┘        └───────────────────┘           
src                                        └──────┘         └───────────────────┘             
typ                                        └──────┘        └───────────────────┘           
doc                                        └──────┘         └───────────────────┘             
921  /- H (colimit F) ⟶ H (colimit G) ⟶ colimit (G ⋙ H) vs
922     H (colimit F) ⟶ colimit (F ⋙ H) ⟶ colimit (G ⋙ H) -/
923    colimit.post F H ≫ H.map (colim.map α) = colim.map (whisker_right α H) ≫ colimit.post G H:=
id     └──────────┘    └──┘  └───┘└──┘    └───┘└──┘  └───────────┘     └──────────┘  
src    └──────────┘       └──┘  └───┘└──┘     └───┘└──┘  └───────────┘       └──────────┘
typ    └──────────┘    └──┘  └───┘└──┘    └───┘└──┘  └───────────┘     └──────────┘  
doc                              └───┘          └───┘
924  begin
st   └─────
925    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
926    rw [←assoc, colimit.ι_post, ←H.map_comp, colim.ι_map, H.map_comp],
id          └───┘  └────────────┘               └─────────┘
src    └───┘└───┘└┘└────────────┘└─┘          └┘└─────────┘└┘          
typ    └───┘└───┘└┘└────────────┘└─┘└────────┘└┘└─────────┘└┘└────────┘
doc    └───┘     └┘              └─┘          └┘           └┘          
txt    └───┘     └┘              └─┘          └┘           └┘          
par    └───┘     └┘              └─┘          └┘           └┘          
pid      └─┘     └┘              └─┘          └┘           └┘          
st   ───────────┘└──────────────┘└───────────┘└───────────┘└──────────┘└──
927    rw [←assoc, colim.ι_map, assoc, colimit.ι_post],
id          └───┘  └─────────┘  └───┘  └────────────┘
src    └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘
typ    └───┘└───┘└┘└─────────┘└┘└───┘└┘└────────────┘
doc    └───┘     └┘           └┘     └┘              
txt    └───┘     └┘           └┘     └┘              
par    └───┘     └┘           └┘     └┘              
pid      └─┘     └┘           └┘     └┘              
st   ───────────┘└───────────┘└─────┘└──────────────┘└──
928    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
929  end
st   └─┘
930  
931  def colim_coyoneda : colim.op ⋙ coyoneda ≅ category_theory.cocones J C :=
id                        └───┘└─┘  └──────┘  └─────────────────────┘  
src                       └───┘└─┘  └──────┘  └─────────────────────┘
typ                       └───┘└─┘  └──────┘  └─────────────────────┘  
doc                       └───┘                └─────────────────────┘
932  nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso (unop F)) (by tidy))
id   └───────────────────┘      └───────────────────┘  └─────────────┘  └──┘ 
src  └───────────────────┘       └───────────────────┘  └─────────────┘  └──┘         └──┘
typ  └───────────────────┘      └───────────────────┘  └─────────────┘  └──┘        └──┘
doc                                                                                   └──┘
txt                                                                                   └──┘
par                                                                                   └──┘
st                                                                                   └───┘
933    (by tidy)
src        └──┘
typ        └──┘
doc        └──┘
txt        └──┘
par        └──┘
st        └───┘
934  
935  end colim_functor
936  
937  def has_colimits_of_shape_of_equivalence {J' : Type v} [small_category J']
id                                                           └────────────┘ └┘
src                                                          └────────────┘
typ                                                          └────────────┘ └┘
doc                                                          └────────────┘
938    (e : J ≌ J') [has_colimits_of_shape J C] : has_colimits_of_shape J' C :=
id            └┘   └───────────────────┘      └───────────────────┘ └┘ 
src                 └───────────────────┘        └───────────────────┘
typ           └┘   └───────────────────┘      └───────────────────┘ └┘ 
doc                 └───────────────────┘        └───────────────────┘
939  by { constructor, intro F, apply has_colimit_of_equivalence_comp e, apply_instance }
id                                    └─────────────────────────────┘ 
src       └─────────┘  └─────┘  └────┘└─────────────────────────────┘   └─────────────┘
typ       └─────────┘  └─────┘  └────┘└─────────────────────────────┘  └─────────────┘
doc       └─────────┘  └─────┘  └────┘                                  └─────────────┘
txt       └─────────┘  └─────┘  └────┘                                  └─────────────┘
par       └─────────┘  └─────┘  └────┘                                  └─────────────┘
pid                         └┘                                                       
st     └────────────┘└───────┘└───────────────────────────────────────┘└───────────────┘└┘
940  
941  end colimit
942  
943  end category_theory.limits